let T be TopSpace; :: thesis: for A being Subset of T
for G being Subset-Family of T st A in G & G is finite-ind holds
A is finite-ind
let A be Subset of T; :: thesis: for G being Subset-Family of T st A in G & G is finite-ind holds
A is finite-ind
let G be Subset-Family of T; :: thesis: ( A in G & G is finite-ind implies A is finite-ind )
assume that
A1: A in G and
A2: G is finite-ind ; :: thesis: A is finite-ind
ex n being Nat st G c= (Seq_of_ind T) . n by A2, Def3;
hence A is finite-ind by A1, Def2; :: thesis: verum