:: deftheorem Def6 defines ind TOPDIM_1:def 6 :
for T being TopSpace
for G being Subset-Family of T st G is finite-ind holds
for b₃ being Integer holds
( b₃ = ind G iff ( G c= (Seq_of_ind T) . (b₃ + 1) & - 1 <= b₃ & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b₃ <= i ) ) );