let T be TopSpace; :: thesis: for G1, G2 being Subset-Family of T st G1 is finite-ind & G2 c= G1 holds
( G2 is finite-ind & ind G2 <= ind G1 )
let G1, G2 be Subset-Family of T; :: thesis: ( G1 is finite-ind & G2 c= G1 implies ( G2 is finite-ind & ind G2 <= ind G1 ) )
assume that
A1: G1 is finite-ind and
A2: G2 c= G1 ; :: thesis: ( G2 is finite-ind & ind G2 <= ind G1 )
A3: - 1 <= ind G1 by A1, Th11;
then for A being Subset of T st A in G2 holds
( A is finite-ind & ind A <= ind G1 ) by A1, A2, Th11;
hence ( G2 is finite-ind & ind G2 <= ind G1 ) by A3, Th11; :: thesis: verum