:: deftheorem defines countably_compact COMPL_SP:def 9 :
for T being TopStruct holds
( T is countably_compact iff for F being Subset-Family of T st F is Cover of T & F is open & F is countable holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) );