---

Step * of Lemma ss-sep_wf

∀[ss:SeparationSpace]. ∀[x,y:Point].  (x # y ∈ ℙ)
BY
{ (Auto THEN D 1 THEN Auto THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[ss:SeparationSpace].  \mforall{}[x,y:Point].    (x  \#  y  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto  THEN  D  1  THEN  Auto  THEN  ProveWfLemma)

---

Home Index