---

Step * of Lemma geo-ge-trivial

No Annotations
∀[g:BasicGeometry]. ∀[a,b:Point].  ab ≥ ab
BY
{ ((Auto THEN Unfold `geo-ge` 0) THEN (D 0 THEN Auto) THEN FLemma `geo-gt-prim-irrefl` [-1] THEN Auto) }

1
.....antecedent..... 
1. g : BasicGeometry
2. a : Point
3. b : Point
4. ab>ab
⊢ BasicGeometryAxioms(g)

---

Latex:

---

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


By

---

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

---

Home Index