defpred S₁[ 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 & S₁[t] ) ) from XFAMILY:sch 1();
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 A8, XBOOLE_1:40;
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 A9, A11, Def2;
B c= A by A8, XBOOLE_1:7;
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