let T be non empty TopSpace; :: thesis: ( T is countably_compact iff 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 )
thus ( T is countably_compact implies 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 ) :: thesis: ( ( 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 ) implies T is countably_compact )

proof

assume T is countably_compact ; :: thesis: 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
then for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite by Th25;
hence 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 Lm3; :: thesis: verum

end;

thus ( ( 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 ) implies T is countably_compact ) by Lm6; :: thesis: verum