---

Step * 1 3 of Lemma euclid-P1


1. e : EuclideanPlane@i'
2. A : Point@i
3. B : Point@i
4. ¬(A = B ∈ Point)
5. C : Point
6. AC=AB ∧ BC=BA
⊢ ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC)
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  A  :  Point@i
3.  B  :  Point@i
4.  \mneg{}(A  =  B)
5.  C  :  Point
6.  AC=AB  \mwedge{}  BC=BA
\mvdash{}  \mexists{}C:Point.  (AC=AB  \mwedge{}  BC=AB  \mwedge{}  AC=BC)


By

---

Latex:
Auto

---

Home Index