Step
*
of Lemma
geo-nontrivial_wf
∀[g:EuclideanPlaneStructure]. (geo-nontrivial(g) ∈ ∃a:Point. (∃b:{Point| a ≠ b}))
BY
{ (ProveWfLemma THEN DRecord 1 THEN Auto) }
Latex:
Latex:
\mforall{}[g:EuclideanPlaneStructure]. (geo-nontrivial(g) \mmember{} \mexists{}a:Point. (\mexists{}b:\{Point| a \mneq{} b\}))
By
Latex:
(ProveWfLemma THEN DRecord 1 THEN Auto)
Home
Index