let T be non empty TopSpace; :: thesis: ( ( for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite ) 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 )
assume A1: for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements 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
let F be Subset-Family of T; :: thesis: ( F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) implies F is finite )
assume that
A2: F is locally_finite and
A3: for A being Subset of T st A in F holds
card A = 1 ; :: thesis: F is finite
not {} T in F by A3, CARD_1:27;
then F is with_non-empty_elements by SETFAM_1:def 8;
hence F is finite by A1, A2; :: thesis: verum