theorem :: TOPDIM_1:29

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 Ga is finite-ind & Ga = G holds
( G is finite-ind & ind G = ind Ga )