let T be TopSpace; :: thesis: for A being Subset of T
for Af being finite-ind Subset of T st A c= Af holds
( A is finite-ind & ind A <= ind Af )
let A be Subset of T; :: thesis: for Af being finite-ind Subset of T st A c= Af holds
( A is finite-ind & ind A <= ind Af )
let Af be finite-ind Subset of T; :: thesis: ( A c= Af implies ( A is finite-ind & ind A <= ind Af ) )
assume A1: A c= Af ; :: thesis: ( A is finite-ind & ind A <= ind Af )
[#] (T | Af) = Af by PRE_TOPC:def 5;
then reconsider A9 = A as Subset of (T | Af) by A1;
A2: ind (T | Af) = ind Af by Lm5;
A3: (T | Af) | A9 = T | A by METRIZTS:9;
hence A is finite-ind by Th18; :: thesis: ind A <= ind Af
then ind (T | A) = ind A by Lm5;
hence ind A <= ind Af by A2, A3, Lm6; :: thesis: verum