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