theorem :: TOPDIM_1:12

for T being TopSpace
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 )