let X be set ; for A being Subset-Family of X holds UniCl (UniCl A) = UniCl A
let A be Subset-Family of X; UniCl (UniCl A) = UniCl A
hereby TARSKI:def 3,
XBOOLE_0:def 10 UniCl A c= UniCl (UniCl A)
let x be
set ;
( x in UniCl (UniCl A) implies x in UniCl A )assume
x in UniCl (UniCl A)
;
x in UniCl Athen 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= x ) } ;
{ y where y is Subset of X : ( y in A & y c= x ) } c= bool X
then reconsider Z =
{ y where y is Subset of X : ( y in A & y c= x ) } as
Subset-Family of
X ;
A3:
x = union Z
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 union Z c= x
let a be
set ;
( a in x implies a in union Z )assume
a in x
;
a in union Zthen 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= x
by A2, A5, ZFMISC_1:74;
then
u c= x
by A10, XBOOLE_1:1;
then
u in Z
by A6, A9;
hence
a in union Z
by A8, TARSKI:def 4;
verum
end;
let a be
set ;
TARSKI:def 3 ( not a in union Z or a in x )
assume
a in union Z
;
a in x
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= x )
by A12;
hence
a in x
by A11;
verum
end;
Z c= A
hence
x in UniCl A
by A3, CANTOR_1:def 1;
verum
end;
thus
UniCl A c= UniCl (UniCl A)
by CANTOR_1:1; verum