---

Step * 1 1 of Lemma eu-add-length-zero


1. e : EuclideanPlane
2. x : Point
3. O_X_x
⊢ (extend Ox by XX) = x ∈ Point
BY
{ ((Assert ¬(O = X ∈ Point) BY
          Auto)
   THEN (Assert ¬(O = x ∈ Point) BY
               ((D 0 THENA Auto) THEN (RevHypSubst (-1) 3 THENA Auto) THEN FLemma `eu-between-eq-same` [3] THEN Auto))
   ) }

1
1. e : EuclideanPlane
2. x : Point
3. O_X_x
4. ¬(O = X ∈ Point)
5. ¬(O = x ∈ Point)
⊢ (extend Ox by XX) = x ∈ Point

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  x  :  Point
3.  O\_X\_x
\mvdash{}  (extend  Ox  by  XX)  =  x


By

---

Latex:
((Assert  \mneg{}(O  =  X)  BY
                Auto)
  THEN  (Assert  \mneg{}(O  =  x)  BY
                          ((D  0  THENA  Auto)
                            THEN  (RevHypSubst  (-1)  3  THENA  Auto)
                            THEN  FLemma  `eu-between-eq-same`  [3]
                            THEN  Auto))
  )

---

Home Index