let X be set ; :: thesis: for A being Subset-Family of X holds UniCl (UniCl A) = UniCl A
let A be Subset-Family of X; :: thesis: UniCl (UniCl A) = UniCl A

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: UniCl A c= UniCl (UniCl A)

let x be object ; :: thesis: ( x in UniCl (UniCl A) implies x in UniCl A )
reconsider xx = x as set by TARSKI:1;
assume x in UniCl (UniCl A) ; :: thesis: x in UniCl A
then consider Y being Subset-Family of X such that
A1: Y c= UniCl A and
A2: x = union Y by CANTOR_1:def 1;
set Z = { y where y is Subset of X : ( y in A & y c= xx ) } ;
{ y where y is Subset of X : ( y in A & y c= xx ) } c= bool X

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Subset of X : ( y in A & y c= xx ) } or a in bool X )
assume a in { y where y is Subset of X : ( y in A & y c= xx ) } ; :: thesis: a in bool X
then ex y being Subset of X st
( a = y & y in A & y c= xx ) ;
hence a in bool X ; :: thesis: verum

end;

then reconsider Z = { y where y is Subset of X : ( y in A & y c= xx ) } as Subset-Family of X ;
A3: xx = union Z

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union Z c= xx

let a be object ; :: thesis: ( a in xx implies a in union Z )
assume a in xx ; :: thesis: a in union Z
then consider s being set such that
A4: a in s and
A5: s in Y by A2, TARSKI:def 4;
consider t being Subset-Family of X such that
A6: t c= A and
A7: s = union t by A1, A5, CANTOR_1:def 1;
consider u being set such that
A8: a in u and
A9: u in t by A4, A7, TARSKI:def 4;
reconsider u = u as Subset of X by A9;
A10: u c= s by A7, A9, ZFMISC_1:74;
s c= xx by A2, A5, ZFMISC_1:74;
then u c= xx by A10;
then u in Z by A6, A9;
hence a in union Z by A8, TARSKI:def 4; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union Z or a in xx )
assume a in union Z ; :: thesis: a in xx
then consider u being set such that
A11: a in u and
A12: u in Z by TARSKI:def 4;
ex y being Subset of X st
( u = y & y in A & y c= xx ) by A12;
hence a in xx by A11; :: thesis: verum

end;

Z c= A

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Z or a in A )
assume a in Z ; :: thesis: a in A
then ex y being Subset of X st
( a = y & y in A & y c= xx ) ;
hence a in A ; :: thesis: verum

end;

hence x in UniCl A by A3, CANTOR_1:def 1; :: thesis: verum

end;

thus UniCl A c= UniCl (UniCl A) by CANTOR_1:1; :: thesis: verum