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 )
assume A1: F is closed_for_countable_unions ; :: thesis: {} in F
reconsider E = {} as countable Subset-Family of T by XBOOLE_1:2;
E c= F by XBOOLE_1:2;
hence {} in F by A1, Def4, ZFMISC_1:2; :: thesis: verum