---

Step * 1 of Lemma eu-le-add1


1. e : EuclideanPlane
2. [p] : {p:Point| O_X_p} 
3. [q] : {p:Point| O_X_p} 
⊢ X_p_(extend Op by Xq)
BY
{ ((Assert ¬(O = X ∈ Point) BY Auto) THEN (Unhide THENA Auto)) }

1
1. e : EuclideanPlane
2. p : {p:Point| O_X_p} 
3. q : {p:Point| O_X_p} 
4. ¬(O = X ∈ Point)
⊢ X_p_(extend Op by Xq)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  [p]  :  \{p:Point|  O\_X\_p\} 
3.  [q]  :  \{p:Point|  O\_X\_p\} 
\mvdash{}  X\_p\_(extend  Op  by  Xq)


By

---

Latex:
((Assert  \mneg{}(O  =  X)  BY  Auto)  THEN  (Unhide  THENA  Auto))

---

Home Index