Step
*
of Lemma
pgeo-point-class_wf
∀[g:ProjectivePlane]. (PointClass ∈ Type)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[g:ProjectivePlane].  (PointClass  \mmember{}  Type)
By
Latex:
ProveWfLemma
Home
Index