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 that
A2: F is Cover of T and
A3: F is open and
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, A3, COMPTS_1:def 1; :: thesis: verum