defpred S₁[ set ] means for t being set st t = $1 holds
( t in Sigma & t c= A & A \ t is thin of P );
consider D being set such that
A1: for t being set holds
( t in D iff ( t in bool Omega & S₁[t] ) ) from XFAMILY:sch 1();
A2: for B being set holds
( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) )

proof

let B be set ; :: thesis: ( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) )
( B in Sigma & B c= A & A \ B is thin of P implies B in D )

proof

assume that
A3: B in Sigma and
A4: ( B c= A & A \ B is thin of P ) ; :: thesis: B in D
for t being set st t = B holds
( t in Sigma & t c= A & A \ t is thin of P ) by A3, A4;
hence B in D by A1, A3; :: thesis: verum

end;

hence ( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) ) by A1; :: thesis: verum

end;

A5: D c= bool Omega

proof

let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in D or B in bool Omega )
assume B in D ; :: thesis: B in bool Omega
then B in Sigma by A2;
hence B in bool Omega ; :: thesis: verum

end;

D <> {}

proof

consider B being set such that
A6: B in Sigma and
A7: ex C being thin of P st A = B \/ C by Def5;
consider C being thin of P such that
A8: A = B \/ C by A7;
consider E being set such that
A9: E in Sigma and
A10: C c= E and
A11: P . E = 0 by Def4;
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 P by A9, A11, Def4;
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 Omega by A5;
take D ; :: thesis: for B being set holds
( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) )
thus for B being set holds
( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) ) by A2; :: thesis: verum