.....assertion.....
Continuous+(L.partial(Unit ⋃ (Top × L)))
{ RepeatFor 2 ((D 0 THENA Auto)) }
1. X : ℕ ⟶ Type
⊢ (⋂n:ℕ. partial(Unit ⋃ (Top × (X n)))) ⊆r partial(Unit ⋃ (Top × (⋂n:ℕ. (X n))))
1. X : ℕ ⟶ Type
⊢ partial(Unit ⋃ (Top × (⋂n:ℕ. (X n)))) ⊆r (⋂n:ℕ. partial(Unit ⋃ (Top × (X n))))