A1: ex B being set st
( B in S & {} c= B & M . B = 0. )
proof
consider B being set such that
A2: ( B = {} & B in S ) by PROB_1:4;
take B ; :: thesis: ( B in S & {} c= B & M . B = 0. )
thus ( B in S & {} c= B & M . B = 0. ) by ; :: thesis: verum
end;
A3: {} is Subset of X by XBOOLE_1:2;
A4: for A being set st A = {} holds
ex B being set st
( B in S & ex C being thin of M st A = B \/ C )
proof
reconsider C = {} as thin of M by A3, A1, Def2;
let A be set ; :: thesis: ( A = {} implies ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) )

consider B being set such that
A5: B = {} and
A6: B in S by PROB_1:4;
assume A = {} ; :: thesis: ex B being set st
( B in S & ex C being thin of M st A = B \/ C )

then A = B \/ C by A5;
hence ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) by A6; :: thesis: verum
end;
defpred S1[ set ] means for A being set st A = \$1 holds
ex B being set st
( B in S & ex C being thin of M st A = B \/ C );
consider D being set such that
A7: for y being set holds
( y in D iff ( y in bool X & S1[y] ) ) from A8: for A being set holds
( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) )
proof
let A be set ; :: thesis: ( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) )

A9: ( A in D iff ( A in bool X & ( for y being set st y = A holds
ex B being set st
( B in S & ex C being thin of M st y = B \/ C ) ) ) ) by A7;
( ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) implies A in D )
proof
assume A10: ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ; :: thesis: A in D
then A c= X by XBOOLE_1:8;
hence A in D by ; :: thesis: verum
end;
hence ( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) by A7; :: thesis: verum
end;
A11: D c= bool X by A7;
{} c= X ;
then reconsider D = D as non empty Subset-Family of X by A7, A11, A4;
take D ; :: thesis: for A being set holds
( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) )

thus for A being set holds
( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) by A8; :: thesis: verum