---

Step * 1 1 of Lemma eu-le-add1


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)
BY
{ ((Assert ¬(O = p ∈ Point) BY
          (DVar `p' THEN Unhide THEN Auto THEN NotEqualFromEuBetween THEN Auto))
   THEN GeneralizeEuExtends [`a']⋅
   ) }

1
1. e : EuclideanPlane
2. p : {p:Point| O_X_p} 
3. q : {p:Point| O_X_p} 
4. ¬(O = X ∈ Point)
5. ¬(O = p ∈ Point)
6. a : Point
7. O_p_a ∧ pa=Xq
⊢ X_p_a

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mneg{}(O  =  p)  BY
                (DVar  `p'  THEN  Unhide  THEN  Auto  THEN  NotEqualFromEuBetween  THEN  Auto))
  THEN  GeneralizeEuExtends  [`a']\mcdot{}
  )

---

Home Index