---

Step * of Lemma ss-fun-sep

∀[X,Y,f,g:Top].  (f # g ~ ∃a:Point(X). f a # g a)
BY
{ (Auto THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[X,Y,f,g:Top].    (f  \#  g  \msim{}  \mexists{}a:Point(X).  f  a  \#  g  a)


By

---

Latex:
(Auto  THEN  Computation)

---

Home Index