---

Step * of Lemma prod-ss-point

∀[ss1,ss2:Top].  (Point(ss1 × ss2) ~ Point(ss1) × Point(ss2))
BY
{ (Auto THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[ss1,ss2:Top].    (Point(ss1  \mtimes{}  ss2)  \msim{}  Point(ss1)  \mtimes{}  Point(ss2))


By

---

Latex:
(Auto  THEN  Computation)

---

Home Index