let T be TopSpace; :: thesis: for A being Subset of T st T is finite-ind holds
A is finite-ind
let A be Subset of T; :: thesis: ( T is finite-ind implies A is finite-ind )
set TA = T | A;
assume T is finite-ind ; :: thesis: A is finite-ind
then T | A is finite-ind by Lm6;
then [#] (T | A) is finite-ind ;
then consider n being Nat such that
A1: [#] (T | A) in (Seq_of_ind (T | A)) . n ;
[#] (T | A) = A by PRE_TOPC:def 5;
then A in (Seq_of_ind T) . n by A1, Th3;
hence A is finite-ind ; :: thesis: verum