---

Step * of Lemma Euclid-Prop28_1

∀e:EuclideanPlane. ∀a,b,c,d,x,y,p:Point.
  (((Colinear(x;a;b) ∧ Colinear(y;c;d)) ∧ (a leftof yx ∧ a-x-b) ∧ (c leftof xy ∧ c-y-d) ∧ p-x-y ∧ bxp ≅a cyx)
  ⇒ geo-parallel-points(e;a;b;c;d))
BY
{ (Auto
   THEN (InstLemma  `vert-angles-congruent` [⌜e⌝;⌜x⌝;⌜b⌝;⌜a⌝;⌜p⌝;⌜y⌝]⋅
         THENA (Auto THEN Unfold `geo-triangle` 0 THEN Auto)
         )
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. p : Point
9. Colinear(x;a;b)
10. Colinear(y;c;d)
11. a leftof yx
12. a-x-b
13. c leftof xy
14. c-y-d
15. p-x-y
16. bxp ≅a cyx
⊢ b # xp

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. p : Point
9. Colinear(x;a;b)
10. Colinear(y;c;d)
11. a leftof yx
12. a-x-b
13. c leftof xy
14. c-y-d
15. p-x-y
16. bxp ≅a cyx
17. bxp ≅a axy
⊢ geo-parallel-points(e;a;b;c;d)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d,x,y,p:Point.
    (((Colinear(x;a;b)  \mwedge{}  Colinear(y;c;d))
    \mwedge{}  (a  leftof  yx  \mwedge{}  a-x-b)
    \mwedge{}  (c  leftof  xy  \mwedge{}  c-y-d)
    \mwedge{}  p-x-y
    \mwedge{}  bxp  \mcong{}\msuba{}  cyx)
    {}\mRightarrow{}  geo-parallel-points(e;a;b;c;d))


By

---

Latex:
(Auto
  THEN  (InstLemma    `vert-angles-congruent`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Unfold  `geo-triangle`  0  THEN  Auto)
              )
  )

---

Home Index