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