---

Step * of Lemma geo-lt-sep

∀e:BasicGeometry. ∀a,b,c,d:Point.  (|ab| < |cd| ⇒ c ≠ d)
BY
{ (Auto THEN RWO "geo-zero-lt-iff<" 0 THEN Auto THEN (Assert 0 ≤ |ab| BY Auto) THEN RWO  "-1<" (-2) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.    (|ab|  <  |cd|  {}\mRightarrow{}  c  \mneq{}  d)


By

---

Latex:
(Auto
  THEN  RWO  "geo-zero-lt-iff<"  0
  THEN  Auto
  THEN  (Assert  0  \mleq{}  |ab|  BY
                          Auto)
  THEN  RWO    "-1<"  (-2)
  THEN  Auto)

---

Home Index