( {} is Subset of X & {{} ,{} } = {{} } ) by ENUMSET1:69, XBOOLE_1:2;
then reconsider C = {{} } as N_Sub_set_fam of X by MEASURE1:41;
take C ; :: thesis: C c= S
{} in S by PROB_1:10;
hence C c= S by ZFMISC_1:37; :: thesis: verum