---

Step * 1 of Lemma euclid-P2


1. e : EuclideanPlane@i'
2. A : Point@i
3. B : Point@i
4. C : Point@i
5. ¬(A = B ∈ Point)
⊢ ∃L:Point. AL=BC
BY
{ (Prolong ⌜B⌝ ⌜A⌝ `L' ⌜B⌝ ⌜C⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  A  :  Point@i
3.  B  :  Point@i
4.  C  :  Point@i
5.  \mneg{}(A  =  B)
\mvdash{}  \mexists{}L:Point.  AL=BC


By

---

Latex:
(Prolong  \mkleeneopen{}B\mkleeneclose{}  \mkleeneopen{}A\mkleeneclose{}  `L'  \mkleeneopen{}B\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index