let T be set ; :: thesis: for F being Subset-Family of T st F is closed_for_countable_unions holds

{} in F

let F be Subset-Family of T; :: thesis: ( F is closed_for_countable_unions implies {} in F )

reconsider E = {} as countable Subset-Family of T by XBOOLE_1:2;

A1: E c= F ;

assume F is closed_for_countable_unions ; :: thesis: {} in F

hence {} in F by A1, ZFMISC_1:2; :: thesis: verum

{} in F

let F be Subset-Family of T; :: thesis: ( F is closed_for_countable_unions implies {} in F )

reconsider E = {} as countable Subset-Family of T by XBOOLE_1:2;

A1: E c= F ;

assume F is closed_for_countable_unions ; :: thesis: {} in F

hence {} in F by A1, ZFMISC_1:2; :: thesis: verum