---

Step * of Lemma geo-length_wf1

∀[e:BasicGeometry]. ∀[s:geo-segment(e)].  (|s| ∈ {p:Point| O_X_p} )
BY
{ (ProveWfLemma
   THEN InstLemma `geo-extend-property` [⌜e⌝;⌜O⌝;⌜X⌝;⌜geo-seg1(s)⌝;⌜geo-seg2(s)⌝;⌜geo-OX-sep(e)⌝]
   THEN Auto{1,1000}-1⋅) }

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[s:geo-segment(e)].    (|s|  \mmember{}  \{p:Point|  O\_X\_p\}  )


By

---

Latex:
(ProveWfLemma
  THEN  InstLemma  `geo-extend-property`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}geo-seg1(s)\mkleeneclose{};\mkleeneopen{}geo-seg2(s)\mkleeneclose{};\mkleeneopen{}geo-OX-sep(e)\mkleeneclose{}]
  THEN  Auto\{1,1000\}-1\mcdot{})

---

Home Index