---

Step * of Lemma eu-seg-length-extend

∀[e:EuclideanPlane]. ∀[s:ProperSegment]. ∀[t:Segment].  (|s + t| = |s| + |t| ∈ {p:Point| O_X_p} )
BY
{ (Auto
   THEN DVar `s'
   THEN RepUR ``eu-seg-proper`` 3
   THEN DVar `s'
   THEN DVar `t'
   THEN RepUR ``eu-seg-extend eu-seg1 eu-seg2`` 0
   THEN All (Fold `eu-mk-seg`)
   THEN All Reduce) }

1
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} 

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[s:ProperSegment].  \mforall{}[t:Segment].    (|s  +  t|  =  |s|  +  |t|)


By

---

Latex:
(Auto
  THEN  DVar  `s'
  THEN  RepUR  ``eu-seg-proper``  3
  THEN  DVar  `s'
  THEN  DVar  `t'
  THEN  RepUR  ``eu-seg-extend  eu-seg1  eu-seg2``  0
  THEN  All  (Fold  `eu-mk-seg`)
  THEN  All  Reduce)

---

Home Index