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