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 set ; :: thesis: ( x in UniCl (UniCl A) implies x in UniCl A )
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 & x = union Y ) by CANTOR_1:def 1;
set Z = { y where y is Subset of X : ( y in A & y c= x ) } ;
{ y where y is Subset of X : ( y in A & y c= x ) } c= bool X

proof

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

end;

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

proof

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

let a be set ; :: thesis: ( a in x implies a in union Z )
assume a in x ; :: thesis: a in union Z
then consider s being set such that
A3: ( a in s & s in Y ) by A1, TARSKI:def 4;
consider t being Subset-Family of X such that
A4: ( t c= A & s = union t ) by A1, A3, CANTOR_1:def 1;
consider u being set such that
A5: ( a in u & u in t ) by A3, A4, TARSKI:def 4;
reconsider u = u as Subset of X by A5;
( u c= s & s c= x ) by A1, A3, A4, A5, ZFMISC_1:92;
then u c= x by XBOOLE_1:1;
then u in Z by A4, A5;
hence a in union Z by A5, TARSKI:def 4; :: thesis: verum

end;

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

end;

Z c= A

proof

let a be set ; :: 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= x ) ;
hence a in A ; :: thesis: verum

end;

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

end;

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