---

Step * of Lemma geo-gt-implies-ge

No Annotations
∀[g:EuclideanPlane]. ∀[c,d,a,b:Point].  cd ≥ ab supposing cd>ab
BY
{ (Auto
   THEN Unfold `geo-ge` 0
   THEN (D 0 THENA Auto)
   THEN (FLemma  `geo-gt-prim-irrefl` [-1] THEN Auto)
   THEN (D 1 THEN Auto)
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[g:EuclideanPlane].  \mforall{}[c,d,a,b:Point].    cd  \mgeq{}  ab  supposing  cd>ab


By

---

Latex:
(Auto
  THEN  Unfold  `geo-ge`  0
  THEN  (D  0  THENA  Auto)
  THEN  (FLemma    `geo-gt-prim-irrefl`  [-1]  THEN  Auto)
  THEN  (D  1  THEN  Auto)
  THEN  Unhide
  THEN  Auto)

---

Home Index