( {} is Subset of X & {{},{}} = {{}} )
by ENUMSET1:29, XBOOLE_1:2;

then reconsider C = {{}} as N_Sub_set_fam of X by MEASURE1:20;

take C ; :: thesis: C c= S

{} in S by PROB_1:4;

hence C c= S by ZFMISC_1:31; :: thesis: verum

then reconsider C = {{}} as N_Sub_set_fam of X by MEASURE1:20;

take C ; :: thesis: C c= S

{} in S by PROB_1:4;

hence C c= S by ZFMISC_1:31; :: thesis: verum