---

Step * of Lemma geo-le-from-be

No Annotations
∀[e:BasicGeometry]. ∀[a,b,c:Point].  |ab| ≤ |ac| supposing B(abc)
BY
{ ((Auto THEN (BLemma `geo-le-iff` THENA Auto)) THEN (D 0 THENA Auto) THEN Unfold `geo-between` -2 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[e:BasicGeometry].  \mforall{}[a,b,c:Point].    |ab|  \mleq{}  |ac|  supposing  B(abc)


By

---

Latex:
((Auto  THEN  (BLemma  `geo-le-iff`  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `geo-between`  -2
  THEN  Auto)

---

Home Index