---

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


1. e : EuclideanPlane
2. x : Point
3. O_X_x
4. y : Point
5. O_X_y
⊢ (extend Ox by Xy) = (extend Oy by Xx) ∈ 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))
   THEN (Assert ¬(O = y ∈ Point) BY
               ((D 0 THENA Auto)
                THEN (RevHypSubst (-1) 5 THENA Auto)
                THEN FLemma `eu-between-eq-same` [5]
                THEN Auto))) }

1
1. e : EuclideanPlane
2. x : Point
3. O_X_x
4. y : Point
5. O_X_y
6. ¬(O = X ∈ Point)
7. ¬(O = x ∈ Point)
8. ¬(O = y ∈ Point)
⊢ (extend Ox by Xy) = (extend Oy by Xx) ∈ Point

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  x  :  Point
3.  O\_X\_x
4.  y  :  Point
5.  O\_X\_y
\mvdash{}  (extend  Ox  by  Xy)  =  (extend  Oy  by  Xx)


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))
  THEN  (Assert  \mneg{}(O  =  y)  BY
                          ((D  0  THENA  Auto)
                            THEN  (RevHypSubst  (-1)  5  THENA  Auto)
                            THEN  FLemma  `eu-between-eq-same`  [5]
                            THEN  Auto)))

---

Home Index