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 ; :: according to COMPL_SP:def 9 :: thesis: ( F is Cover of & F is open & F is countable implies ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite ) )
assume that
A2: F is Cover of and
A3: F is open and
F is countable ; :: thesis: ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite )
thus ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite ) by A1, A2, A3, COMPTS_1:def 3; :: thesis: verum