let X be set ; :: thesis: bool X is SigmaField of X
A1: for M being N_Sub_set_fam of X st M c= bool X holds
union M in bool X ;
reconsider Y = bool X as Subset-Family of X ;
for A being set st A in bool X holds
X \ A in bool X ;
then reconsider Y = Y as non empty compl-closed sigma-additive Subset-Family of X by A1, MEASURE1:def 1, MEASURE1:def 5;
Y is SigmaField of X ;
hence bool X is SigmaField of X ; :: thesis: verum