---

Step * of Lemma geo-ge-trivial2

No Annotations
∀[g:BasicGeometry]. ∀[a,b,c:Point].  ab ≥ cc
BY
{ (Auto THEN Unfold `geo-ge` 0 THEN (D 1 THEN Auto) THEN D 2 THEN ExRepD) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[g:BasicGeometry].  \mforall{}[a,b,c:Point].    ab  \mgeq{}  cc


By

---

Latex:
(Auto  THEN  Unfold  `geo-ge`  0  THEN  (D  1  THEN  Auto)  THEN  D  2  THEN  ExRepD)

---

Home Index