{ (union P) where P is Subset of D : verum } c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (union P) where P is Subset of D : verum } ; :: thesis:
then consider P being Subset of D such that
A1: x = union P ;
union P c= union D by ZFMISC_1:77;
then union P c= X by EQREL_1:def 4;
hence x in bool X by A1; :: thesis:

end;

then reconsider DU = { (union P) where P is Subset of D : verum } as Subset-Family of X ;
for a being Subset-Family of X st a c= DU holds
union a in DU

proof

let a be Subset-Family of X; :: thesis:
assume A2: a c= DU ; :: thesis:
set P = { x where x is Element of D : x c= union a } ;

per cases ;

suppose A3: D = {} ; :: thesis:

then UniCl D = {{}} by Th16;
then a c= {{}} by A2, Th14;
then ( a = {} or a = {{}} ) by ZFMISC_1:33;
hence union a in DU by A3, ZFMISC_1:2; :: thesis:

end;

suppose A4: D <> {} ; :: thesis:

{ x where x is Element of D : x c= union a } c= D

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in { x where x is Element of D : x c= union a } ; :: thesis:
then ex x being Element of D st
( t = x & x c= union a ) ;
hence t in D by A4; :: thesis:

end;

then reconsider P = { x where x is Element of D : x c= union a } as Subset of D ;
union a = union P

proof

thus union a c= union P :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union a ; :: thesis:
then consider t being set such that
A6: x in t and
A7: t in a by TARSKI:def 4;
t in DU by A2, A7;
then consider Q being Subset of D such that
A8: t = union Q ;
consider y being set such that
A9: x in y and
A10: y in Q by A6, A8, TARSKI:def 4;
reconsider y = y as Element of D by A10;
y c= union a

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in y ; :: thesis:
then b in union Q by A10, TARSKI:def 4;
hence b in union a by A7, A8, TARSKI:def 4; :: thesis:

end;

then y in P ;
hence x in union P by A9, TARSKI:def 4; :: thesis:

end;

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in union P ; :: thesis:
then consider u being set such that
A11: t in u and
A12: u in P by TARSKI:def 4;
ex xu being Element of D st
( u = xu & xu c= union a ) by A12;
hence t in union a by A11; :: thesis:

end;

hence union a in DU ; :: thesis:

end;

end;

end;

then DU is union-closed ;
hence UniCl D is union-closed by Th14; :: thesis: