---

Step * of Lemma geo-lt-iff-strict-between

∀g:EuclideanPlane. ∀s1,s2:geo-segment(g).  (|s1| < |s2| ⇐⇒ X_|s1|_|s2| ∧ |s1| ≠ |s2|)
BY
{ (Intros
   THEN (RWO "geo-le-iff-between<" 0 THENA Auto)
   THEN InstLemma `geo-lt-iff-strict-between-points` [⌜g⌝;⌜|s1|⌝;⌜|s2|⌝]⋅
   THEN Auto) }

---

Latex:

---

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


By

---

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

---

Home Index