---

Step * of Lemma subtype-geo-length-type

∀[e:BasicGeometry]. ({p:Point| O_X_p}  ⊆r Length)
BY
{ (Unfold `geo-length-type` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  (\{p:Point|  O\_X\_p\}    \msubseteq{}r  Length)


By

---

Latex:
(Unfold  `geo-length-type`  0  THEN  Auto)

---

Home Index