let G be Subset-Family of T; :: thesis: ( G is empty implies G is with_finite_small_inductive_dimension )
assume G is empty ; :: thesis: G is with_finite_small_inductive_dimension
then A1: G c= {({} T)} by XBOOLE_1:2;
(Seq_of_ind T) . 0 = {({} T)} by Def1;
hence G is with_finite_small_inductive_dimension by A1, Def3; :: thesis: verum