---

Step * 3 of Lemma r2-basic-geo-axioms


∀a,b,c:Point.  bc ≥ aa
BY
{ ((UnfoldGeoAbbreviations 0 THEN Auto)
   THEN RWO "real-vec-dist-same-zero" 0
   THEN Auto
   THEN (Assert r0 ≤ d(b;c) BY
               Auto)
   THEN Auto) }

---

Latex:

---

Latex:

\mforall{}a,b,c:Point.    bc  \mgeq{}  aa


By

---

Latex:
((UnfoldGeoAbbreviations  0  THEN  Auto)
  THEN  RWO  "real-vec-dist-same-zero"  0
  THEN  Auto
  THEN  (Assert  r0  \mleq{}  d(b;c)  BY
                          Auto)
  THEN  Auto)

---

Home Index