---

Step * of Lemma strong-continuous-set

∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[F:Type ⟶ Type].
  (Continuous+(T.{x:F[T]| P[x]} )) supposing (Continuous+(T.F[T]) and (∀T:Type. (F[T] ⊆r A)))
BY
{ (Unfold `so_apply` 0
   THEN Auto
   THEN RepeatFor 4 (ParallelLast)
   THEN D 0
   THEN Auto
   THEN (Assert x ∈ {x:F (X 0)| P x}  BY
               (With ⌜0⌝ (D (-1))⋅ THEN Auto))⋅
   THEN (MemTypeHD (-1) THENA Auto)
   THEN (MemTypeCD THENA Auto)
   THEN SubsumeC ⌜⋂n:ℕ. (F (X n))⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[F:Type  {}\mrightarrow{}  Type].
    (Continuous+(T.\{x:F[T]|  P[x]\}  ))  supposing  (Continuous+(T.F[T])  and  (\mforall{}T:Type.  (F[T]  \msubseteq{}r  A)))


By

---

Latex:
(Unfold  `so\_apply`  0
  THEN  Auto
  THEN  RepeatFor  4  (ParallelLast)
  THEN  D  0
  THEN  Auto
  THEN  (Assert  x  \mmember{}  \{x:F  (X  0)|  P  x\}    BY
                          (With  \mkleeneopen{}0\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto))\mcdot{}
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  (MemTypeCD  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}\mcap{}n:\mBbbN{}.  (F  (X  n))\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index