Step
*
of Lemma
geo-length_wf
∀[e:BasicGeometry]. ∀[s:geo-segment(e)].  (|s| ∈ Length)
BY
{ Auto }
Latex:
Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[s:geo-segment(e)].    (|s|  \mmember{}  Length)
By
Latex:
Auto
Home
Index