:: deftheorem Def5 defines ind TOPDIM_1:def 5 :
for T being TopSpace
for A being Subset of T st A is finite-ind holds
for b₃ being Integer holds
( b₃ = ind A iff ( A in (Seq_of_ind T) . (b₃ + 1) & not A in (Seq_of_ind T) . b₃ ) );