theorem :: TOPDIM_1:30

for T being TopSpace
for A being Subset of T
for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st G is finite-ind & Ga = G holds
( Ga is finite-ind & ind G = ind Ga )