---

Step * 1 2 1 1 of Lemma e1


1. e : EuclideanPlane@i'
2. A : Point@i
3. B : Point@i
4. ¬(A = B ∈ Point)
5. q : Point
6. A_B_q ∧ Bq=AB
⊢ A_A_B ∧ A_B_q ∧ AA=AA ∧ Aq=Aq ∧ BA=BA ∧ Bq=BA
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  A  :  Point@i
3.  B  :  Point@i
4.  \mneg{}(A  =  B)
5.  q  :  Point
6.  A\_B\_q  \mwedge{}  Bq=AB
\mvdash{}  A\_A\_B  \mwedge{}  A\_B\_q  \mwedge{}  AA=AA  \mwedge{}  Aq=Aq  \mwedge{}  BA=BA  \mwedge{}  Bq=BA


By

---

Latex:
Auto

---

Home Index