let T be non empty TopSpace; :: thesis: ( 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 )
thus ( T is countably_compact implies for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite ) by Lm2; :: thesis: ( ( for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite ) implies T is countably_compact )
assume for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite ; :: thesis: T is countably_compact
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 Lm3;
hence T is countably_compact by Lm6; :: thesis: verum