defpred S1[ set ] means for t being set st t = \$1 holds
( t in S & t c= A & A \ t is thin of M );
consider D being set such that
A1: for t being set holds
( t in D iff ( t in bool X & S1[t] ) ) from A2: for B being set holds
( B in D iff ( B in S & B c= A & A \ B is thin of M ) )
proof
let B be set ; :: thesis: ( B in D iff ( B in S & B c= A & A \ B is thin of M ) )
( B in S & B c= A & A \ B is thin of M implies B in D )
proof
assume that
A3: B in S and
A4: ( B c= A & A \ B is thin of M ) ; :: thesis: B in D
for t being set st t = B holds
( t in S & t c= A & A \ t is thin of M ) by A3, A4;
hence B in D by A1, A3; :: thesis: verum
end;
hence ( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) by A1; :: thesis: verum
end;
A5: D c= bool X
proof
let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in D or B in bool X )
assume B in D ; :: thesis: B in bool X
then B in S by A2;
hence B in bool X ; :: thesis: verum
end;
D <> {}
proof
consider B being set such that
A6: B in S and
A7: ex C being thin of M st A = B \/ C by Def3;
consider C being thin of M such that
A8: A = B \/ C by A7;
consider E being set such that
A9: E in S and
A10: C c= E and
A11: M . E = 0. by Def2;
A \ B = C \ B by ;
then A \ B c= C by XBOOLE_1:36;
then A \ B c= E by A10;
then A12: A \ B is thin of M by ;
B c= A by ;
hence D <> {} by A2, A6, A12; :: thesis: verum
end;
then reconsider D = D as non empty Subset-Family of X by A5;
take D ; :: thesis: for B being set holds
( B in D iff ( B in S & B c= A & A \ B is thin of M ) )

thus for B being set holds
( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) by A2; :: thesis: verum