let X be set ; :: thesis: for Si being SigmaField of X ex A being Subset of X st A in Si
let Si be SigmaField of X; :: thesis: ex A being Subset of X st A in Si
consider A being Element of Si;
( A in Si & Si c= bool X ) ;
hence ex A being Subset of X st A in Si ; :: thesis: verum