---

Step * of Lemma eu-seg-length-test2

∀e:EuclideanPlane. ∀s1,s2:ProperSegment. ∀t1,t2,t3:Segment.  (s1 ≡ s2 ⇒ t1 ≡ t2 ⇒ t2 ≡ t3 ⇒ s1 + t1 ≡ s2 + t3)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}s1,s2:ProperSegment.  \mforall{}t1,t2,t3:Segment.
    (s1  \mequiv{}  s2  {}\mRightarrow{}  t1  \mequiv{}  t2  {}\mRightarrow{}  t2  \mequiv{}  t3  {}\mRightarrow{}  s1  +  t1  \mequiv{}  s2  +  t3)


By

---

Latex:
Auto

---

Home Index