---

Step * 1 of Lemma geo-add-length-property1


1. g : EuclideanPlane
2. p : {p:Point| B(OXp)} 
3. q : {p:Point| B(OXp)} 
⊢ B(Xpp + q)
BY
{ (Unfold `geo-add-length` 0 THEN (GenConclTerm ⌜extend Op by Xq⌝⋅ THENA Auto) THEN DSetVars THEN Unhide THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  p  :  \{p:Point|  B(OXp)\} 
3.  q  :  \{p:Point|  B(OXp)\} 
\mvdash{}  B(Xpp  +  q)


By

---

Latex:
(Unfold  `geo-add-length`  0
  THEN  (GenConclTerm  \mkleeneopen{}extend  Op  by  Xq\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  DSetVars
  THEN  Unhide
  THEN  Auto)

---

Home Index