---

Step * of Lemma geo-add-length-property2

∀g:EuclideanPlane. ∀s:geo-segment(g). ∀c,d:Point.  cd ≅ |s||s| + |cd|
BY
{ (Auto THEN (GenConcl ⌜|s| = p ∈ {p:Point| O_X_p} ⌝⋅ THENA Auto) THEN ThinVar `s') }

1
1. g : EuclideanPlane
2. c : Point
3. d : Point
4. p : {p:Point| O_X_p} 
⊢ cd ≅ pp + |cd|

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}s:geo-segment(g).  \mforall{}c,d:Point.    cd  \mcong{}  |s||s|  +  |cd|


By

---

Latex:
(Auto  THEN  (GenConcl  \mkleeneopen{}|s|  =  p\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `s')

---

Home Index