let T be TopStruct ; :: thesis: ( T is compact implies T is countably_compact )
assume A1: T is compact ; :: thesis: T is countably_compact
let F be Subset-Family of T; :: according to COMPL_SP:def 9 :: thesis: ( F is Cover of T & F is open & F is countable implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) )
assume A2: ( F is Cover of T & F is open & F is countable ) ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite )
thus ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) by A1, A2, COMPTS_1:def 3; :: thesis: verum