A1: {} is thin of P by Th24;
A2: 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 ) )
consider B being set such that
A3: B = {} and
A4: B in Sigma by PROB_1:4;
consider C being thin of P such that
A5: C = {} by A1;
assume A = {} ; :: thesis: ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C )
then A = B \/ C by A3, A5;
hence ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) by A4; :: thesis: verum

end;

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
A6: for y being set holds
( y in D iff ( y in bool Omega & S₁[y] ) ) from XFAMILY:sch 1();
A7: 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 ) )
A8: ( 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 A6;
( ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) implies A in D )

proof

assume A9: ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ; :: thesis: A in D
then A c= Omega by XBOOLE_1:8;
hence A in D by A8, A9; :: 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 A6; :: thesis: verum

end;

A10: D c= bool Omega by A6;
{} c= Omega ;
then reconsider D = D as non empty Subset-Family of Omega by A6, A10, A2;
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 A7; :: thesis: verum