theorem :: TOPDIM_1:17
for T being TopSpace
for Af being finite-ind Subset of T holds ind (T | Af) = ind Af by Lm5;