for T being non empty TopSpace holds
( T is countably_compact iff for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite )