Step
*
of Lemma
eu-point_wf
∀[e:EuclideanStructure]. (Point ∈ Type)
BY
{ (ProveWfLemma THEN DRecord 1 THEN Auto) }
Latex:
Latex:
\mforall{}[e:EuclideanStructure]. (Point \mmember{} Type)
By
Latex:
(ProveWfLemma THEN DRecord 1 THEN Auto)
Home
Index