for T being non empty TopSpace holds
( 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 )