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 ;
( 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 = {}
;
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;
verum
end;
defpred S1[ 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 & S1[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 ;
( 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 )
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;
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
; 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; verum