---

Step * 1 of Lemma eu-seg-length-extend


1. e : EuclideanPlane
2. s1 : Point
3. s2 : Point
4. ¬(s1 = s2 ∈ Point)
5. t1 : Point
6. t2 : Point
⊢ |s1(extend s1s2 by t1t2)| = |s1s2| + |t1t2| ∈ {p:Point| O_X_p} 
BY
{ (GeneralizeEuExtends [`a'] THEN InstLemma `eu-add-length-between` [⌜e⌝;⌜s1⌝;⌜s2⌝;⌜a⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  s1  :  Point
3.  s2  :  Point
4.  \mneg{}(s1  =  s2)
5.  t1  :  Point
6.  t2  :  Point
\mvdash{}  |s1(extend  s1s2  by  t1t2)|  =  |s1s2|  +  |t1t2|


By

---

Latex:
(GeneralizeEuExtends  [`a']  THEN  InstLemma  `eu-add-length-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}s1\mkleeneclose{};\mkleeneopen{}s2\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index