let X be set ; :: thesis: ex F being subset-closed set st
( F = union { (bool x) where x is Element of X : x in X } & X c= F & ( for Y being set st X c= Y & Y is subset-closed holds
F c= Y ) )
set B = { (bool x) where x is Element of X : x in X } ;

now :: thesis: for a, b being set st a in union { (bool x) where x is Element of X : x in X } & b c= a holds
b in union { (bool x) where x is Element of X : x in X }

let a, b be set ; :: thesis: ( a in union { (bool x) where x is Element of X : x in X } & b c= a implies b in union { (bool x) where x is Element of X : x in X } )
assume that
A1: a in union { (bool x) where x is Element of X : x in X } and
A2: b c= a ; :: thesis: b in union { (bool x) where x is Element of X : x in X }
consider y being set such that
A3: a in y and
A4: y in { (bool x) where x is Element of X : x in X } by A1, TARSKI:def 4;
consider x being Element of X such that
A5: y = bool x and
x in X by A4;
b c= x by A2, A3, A5, XBOOLE_1:1;
hence b in union { (bool x) where x is Element of X : x in X } by A4, A5, TARSKI:def 4; :: thesis: verum

end;

then reconsider U = union { (bool x) where x is Element of X : x in X } as subset-closed set by CLASSES1:def 1;
take U ; :: thesis: ( U = union { (bool x) where x is Element of X : x in X } & X c= U & ( for Y being set st X c= Y & Y is subset-closed holds
U c= Y ) )
thus U = union { (bool x) where x is Element of X : x in X } ; :: thesis: ( X c= U & ( for Y being set st X c= Y & Y is subset-closed holds
U c= Y ) )
thus X c= U :: thesis: for Y being set st X c= Y & Y is subset-closed holds
U c= Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in U )
assume A6: x in X ; :: thesis: x in U
reconsider xx = x as set by TARSKI:1;
( xx c= xx & bool xx in { (bool x) where x is Element of X : x in X } ) by A6;
hence x in U by TARSKI:def 4; :: thesis: verum

end;

let Y be set ; :: thesis: ( X c= Y & Y is subset-closed implies U c= Y )
assume A7: ( X c= Y & Y is subset-closed ) ; :: thesis: U c= Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in U or x in Y )
assume x in U ; :: thesis: x in Y
then consider y being set such that
A8: x in y and
A9: y in { (bool x) where x is Element of X : x in X } by TARSKI:def 4;
ex x being Element of X st
( y = bool x & x in X ) by A9;
hence x in Y by A7, A8; :: thesis: verum