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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in bool Omega )
assume x in D ; :: thesis: x in bool Omega
hence x in bool Omega by A1; :: thesis: verum

end;

A3: for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )

proof

let A be set ; :: thesis: ( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )
A4: ( A in D iff ( A in bool Omega & ( for y being set st y = A holds
ex B being set st
( B in Sigma & ex C being thin of P st y = B \/ C ) ) ) ) by A1;
( ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) implies A in D )

proof

assume A5: ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ; :: thesis: A in D
then consider B being set such that
A6: ( B in Sigma & ex C being thin of P st A = B \/ C ) ;
A c= Omega by A6, XBOOLE_1:8;
hence A in D by A4, A5; :: thesis: verum

end;

hence ( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) by A1; :: thesis: verum

end;

A7: {} is thin of P by Th25;
A8: {} c= Omega by XBOOLE_1:2;
for A being set st A = {} holds
ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C )

proof

let A be set ; :: thesis: ( A = {} implies ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )
assume A9: A = {} ; :: thesis: ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C )
consider B being set such that
A10: ( B = {} & B in Sigma ) by PROB_1:42;
consider C being thin of P such that
A11: C = {} by A7;
A = B \/ C by A9, A10, A11;
hence ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) by A10; :: thesis: verum

end;

then reconsider D = D as non empty Subset-Family of Omega by A1, A2, A8;
take D ; :: thesis: for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )
thus for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) by A3; :: thesis: verum