Step
*
of Lemma
eu-mk-seg_wf
∀[e:EuclideanStructure]. ∀[a,b:Point].  (ab ∈ Segment)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[e:EuclideanStructure].  \mforall{}[a,b:Point].    (ab  \mmember{}  Segment)
By
Latex:
ProveWfLemma
Home
Index