(Seq_of_ind T) . 0 = {({} T)} by Def1;
then {({} T)} is with_finite_small_inductive_dimension by Def3;
hence ex b₁ being Subset-Family of T st
( not b₁ is empty & b₁ is with_finite_small_inductive_dimension ) ; :: thesis: verum