---

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


1. e : EuclideanPlane
2. x : Point
3. O_X_x
4. ¬(O = X ∈ Point)
5. ¬(O = x ∈ Point)
⊢ (extend Ox by XX) = x ∈ Point
BY
{ ((InstLemma `eu-extend-property` [⌜e⌝;⌜O⌝;⌜x⌝;⌜X⌝;⌜X⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerm ⌜(extend Ox by XX)⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `eu-extend-property`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerm  \mkleeneopen{}(extend  Ox  by  XX)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index