---

Step * 1 2 of Lemma euclid-P1

.....antecedent..... 
1. e : EuclideanPlane@i'
2. A : Point@i
3. B : Point@i
4. ¬(A = B ∈ Point)
⊢ ∃p,q,x,z:Point. (A_x_B ∧ A_B_z ∧ Ap=Ax ∧ Aq=Az ∧ Bp=BA ∧ Bq=BA)
BY
{ (Prolong ⌜A⌝ ⌜B⌝ `q' ⌜A⌝ ⌜B⌝⋅ 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
⊢ ∃p,q,x,z:Point. (A_x_B ∧ A_B_z ∧ Ap=Ax ∧ Aq=Az ∧ Bp=BA ∧ Bq=BA)

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  EuclideanPlane@i'
2.  A  :  Point@i
3.  B  :  Point@i
4.  \mneg{}(A  =  B)
\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:
(Prolong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}  `q'  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index