let T be non empty T_1 TopSpace; :: thesis: ( T is countably_compact iff for A being Subset of T st A is infinite holds
not Der A is empty )
thus ( T is countably_compact implies for A being Subset of T st A is infinite holds
not Der A is empty ) :: thesis: ( ( for A being Subset of T st A is infinite holds
not Der A is empty ) implies T is countably_compact )

proof

assume T is countably_compact ; :: thesis: for A being Subset of T st A is infinite holds
not Der A is empty
then for F being Subset-Family of T st F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite by Th26;
hence for A being Subset of T st A is infinite holds
not Der A is empty by Lm4; :: thesis: verum

end;

assume for A being Subset of T st A is infinite holds
not Der A is empty ; :: thesis: T is countably_compact
then for A being Subset of T st A is infinite & A is countable holds
not Der A is empty ;
hence T is countably_compact by Lm5; :: thesis: verum