theorem :: COMPL_SP:29
for T being non empty T_1 TopSpace holds
( T is countably_compact iff for A being Subset of T st A is infinite & A is countable holds
not Der A is empty ) by Lm5, Th27;