let T be TopSpace; :: thesis: for G being Subset-Family of T holds
( ( ind G = - 1 & G is with_finite_small_inductive_dimension ) iff G c= {({} T)} )
let G be Subset-Family of T; :: thesis: ( ( ind G = - 1 & G is with_finite_small_inductive_dimension ) iff G c= {({} T)} )
A1: {({} T)} = (Seq_of_ind T) . 0 by Def1;
0 = (- 1) + 1 ;
hence ( ind G = - 1 & G is with_finite_small_inductive_dimension implies G c= {({} T)} ) by A1, Def6; :: thesis: ( G c= {({} T)} implies ( ind G = - 1 & G is with_finite_small_inductive_dimension ) )
assume A2: G c= {({} T)} ; :: thesis: ( ind G = - 1 & G is with_finite_small_inductive_dimension )
then A3: G is with_finite_small_inductive_dimension by A1, Def3;
then A4: - 1 <= ind G by Def6;
0 = (- 1) + 1 ;
then ind G <= - 1 by A1, A2, A3, Def6;
hence ( ind G = - 1 & G is with_finite_small_inductive_dimension ) by A1, A2, A4, Def3, XXREAL_0:1; :: thesis: verum