---

Step * 1 2 1 of Lemma euclid-P1


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
⊢ ∃p,q,x,z:Point. (A_x_B ∧ A_B_z ∧ Ap=Ax ∧ Aq=Az ∧ Bp=BA ∧ Bq=BA)
BY
{ (InstConcl [⌜A⌝;⌜q⌝;⌜A⌝;⌜q⌝]⋅ THENA Auto) }

1
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

---

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{}  \mexists{}p,q,x,z:Point.  (A\_x\_B  \mwedge{}  A\_B\_z  \mwedge{}  Ap=Ax  \mwedge{}  Aq=Az  \mwedge{}  Bp=BA  \mwedge{}  Bq=BA)


By

---

Latex:
(InstConcl  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index