:: deftheorem Def1 defines Seq_of_ind TOPDIM_1:def 1 :
for T being TopSpace
for b₂ being SetSequence of (bool the carrier of T) holds
( b₂ = Seq_of_ind T iff for A being Subset of T
for n being Nat holds
( b₂ . 0 = {({} T)} & ( not A in b₂ . (n + 1) or A in b₂ . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b₂ . n ) ) & ( ( A in b₂ . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b₂ . n ) ) implies A in b₂ . (n + 1) ) ) );