( {} 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