---

Step * 1 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
6. ¬(O = X ∈ Point)
7. ¬(O = x ∈ Point)
8. ¬(O = y ∈ Point)
⊢ (extend Ox by Xy) = (extend Oy by Xx) ∈ Point
BY
{ (((InstLemma `eu-extend-property` [⌜e⌝;⌜O⌝;⌜x⌝;⌜X⌝;⌜y⌝]⋅ THENA Auto)
    THEN MoveToConcl (-1)
    THEN (GenConclTerm ⌜(extend Ox by Xy)⌝⋅ THENA Auto)
    THEN Thin (-1)
    THEN RenameVar `a' (-1))
   THEN (InstLemma `eu-extend-property` [⌜e⌝;⌜O⌝;⌜y⌝;⌜X⌝;⌜x⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜(extend Oy by Xx)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `b' (-1)
   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)
9. a : Point
10. b : Point
11. O_y_b
12. yb=Xx
13. O_x_a
14. xa=Xy
⊢ a = b ∈ Point

---

Latex:

---

Latex:

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


By

---

Latex:
(((InstLemma  `eu-extend-property`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  MoveToConcl  (-1)
    THEN  (GenConclTerm  \mkleeneopen{}(extend  Ox  by  Xy)\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  Thin  (-1)
    THEN  RenameVar  `a'  (-1))
  THEN  (InstLemma  `eu-extend-property`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}(extend  Oy  by  Xx)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `b'  (-1)
  THEN  Auto)

---

Home Index