---

Step * of Lemma geo-le-iff-between

∀g:EuclideanPlane. ∀s1,s2:geo-segment(g).  (|s1| ≤ |s2| ⇐⇒ X_|s1|_|s2|)
BY
{ (Intros THEN InstLemma `geo-le-iff-between-points` [⌜g⌝;⌜|s1|⌝;⌜|s2|⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}s1,s2:geo-segment(g).    (|s1|  \mleq{}  |s2|  \mLeftarrow{}{}\mRightarrow{}  X\_|s1|\_|s2|)


By

---

Latex:
(Intros  THEN  InstLemma  `geo-le-iff-between-points`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}|s1|\mkleeneclose{};\mkleeneopen{}|s2|\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index