---

Step * of Lemma prod-ss_wf

∀[ss1,ss2:SeparationSpace].  (ss1 × ss2 ∈ SeparationSpace)
BY
{ (Auto
   THEN (Assert ss1 ∈ SeparationSpace BY
               Auto)
   THEN (Assert ss2 ∈ SeparationSpace BY
               Auto)
   THEN (D 2 THENA Auto)
   THEN (D 1 THENA Auto)
   THEN All (Folds ``ss-point ss-sep``)
   THEN Unfold `prod-ss` 0
   THEN MemCD
   THEN Try ((MemTypeCD
              THEN Reduce 0
              THEN Auto
              THEN D -1
              THEN Reduce 0
              THEN (D 0 THENA Auto)
              THEN D -1
              THEN MoveToConcl (-1)
              THEN Fold `not` 0
              THEN Auto))
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[ss1,ss2:SeparationSpace].    (ss1  \mtimes{}  ss2  \mmember{}  SeparationSpace)


By

---

Latex:
(Auto
  THEN  (Assert  ss1  \mmember{}  SeparationSpace  BY
                          Auto)
  THEN  (Assert  ss2  \mmember{}  SeparationSpace  BY
                          Auto)
  THEN  (D  2  THENA  Auto)
  THEN  (D  1  THENA  Auto)
  THEN  All  (Folds  ``ss-point  ss-sep``)
  THEN  Unfold  `prod-ss`  0
  THEN  MemCD
  THEN  Try  ((MemTypeCD
                        THEN  Reduce  0
                        THEN  Auto
                        THEN  D  -1
                        THEN  Reduce  0
                        THEN  (D  0  THENA  Auto)
                        THEN  D  -1
                        THEN  MoveToConcl  (-1)
                        THEN  Fold  `not`  0
                        THEN  Auto))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index