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

per cases ( A = {} or A <> {} ) ;

suppose A1: A = {} ; :: thesis: UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)

then A2: FinMeetCl A = {X} by Th17;
UniCl A = {{}} by A1, Th16;
then A3: FinMeetCl (UniCl A) = {{},X} by Th11;
UniCl (FinMeetCl A) = {X,{}} by A2, Th11;
hence UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A) by A3, Th18; :: thesis: verum

end;

suppose A <> {} ; :: thesis: UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)

then reconsider A = A as non empty Subset-Family of X ;
A4: UniCl (FinMeetCl (UniCl A)) c= UniCl (UniCl (FinMeetCl A))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UniCl (FinMeetCl (UniCl A)) or x in UniCl (UniCl (FinMeetCl A)) )
assume x in UniCl (FinMeetCl (UniCl A)) ; :: thesis: x in UniCl (UniCl (FinMeetCl A))
then consider Y being Subset-Family of X such that
A5: Y c= FinMeetCl (UniCl A) and
A6: x = union Y by CANTOR_1:def 1;
Y c= UniCl (FinMeetCl A)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in UniCl (FinMeetCl A) )
assume y in Y ; :: thesis: y in UniCl (FinMeetCl A)
then consider Z being Subset-Family of X such that
A7: Z c= UniCl A and
A8: Z is finite and
A9: y = Intersect Z by A5, CANTOR_1:def 3;

per cases ( Z = {} or Z <> {} ) ;

suppose Z = {} ; :: thesis: y in UniCl (FinMeetCl A)

then y = X by A9, SETFAM_1:def 9;
then A10: y in FinMeetCl A by CANTOR_1:8;
FinMeetCl A c= UniCl (FinMeetCl A) by CANTOR_1:1;
hence y in UniCl (FinMeetCl A) by A10; :: thesis: verum

end;

suppose A11: Z <> {} ; :: thesis: y in UniCl (FinMeetCl A)

then A12: y = meet Z by A9, SETFAM_1:def 9;
set G = { (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z } ;
A13: { (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z } c= FinMeetCl A

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z } or a in FinMeetCl A )
assume a in { (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z } ; :: thesis: a in FinMeetCl A
then consider f being Element of Funcs (Z,A) such that
A14: a = meet (rng f) and
for z being set st z in Z holds
f . z c= z ;
reconsider B = rng f as Subset-Family of X by XBOOLE_1:1;
reconsider B = B as Subset-Family of X ;
Intersect B = a by A11, A14, SETFAM_1:def 9;
hence a in FinMeetCl A by A8, CANTOR_1:def 3; :: thesis: verum

end;

then reconsider G = { (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z } as Subset-Family of X by XBOOLE_1:1;
reconsider G = G as Subset-Family of X ;
union G = y

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: y c= union G

let a be set ; :: thesis: ( a in union G implies a in y )
assume a in union G ; :: thesis: a in y
then consider b being set such that
A15: a in b and
A16: b in G by TARSKI:def 4;
consider f being Element of Funcs (Z,A) such that
A17: b = meet (rng f) and
A18: for z being set st z in Z holds
f . z c= z by A16;
A19: dom f = Z by FUNCT_2:def 1;
reconsider B = rng f as Subset-Family of X by XBOOLE_1:1;
reconsider B = B as Subset-Family of X ;
b c= y

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in b or c in y )
assume A20: c in b ; :: thesis: c in y

now

let d be set ; :: thesis: ( d in Z implies c in d )
assume A21: d in Z ; :: thesis: c in d
then f . d in B by A19, FUNCT_1:def 3;
then A22: b c= f . d by A17, SETFAM_1:3;
A23: f . d c= d by A18, A21;
c in f . d by A20, A22;
hence c in d by A23; :: thesis: verum

end;

hence c in y by A11, A12, SETFAM_1:def 1; :: thesis: verum

end;

hence a in y by A15; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in y or a in union G )
assume A24: a in y ; :: thesis: a in union G
defpred S₁[ set , set ] means ( a in $2 & $2 c= $1 );

A25: now

let z be set ; :: thesis: ( z in Z implies ex w being set st
( w in A & S₁[z,w] ) )
assume A26: z in Z ; :: thesis: ex w being set st
( w in A & S₁[z,w] )
then A27: a in z by A12, A24, SETFAM_1:def 1;
consider C being Subset-Family of X such that
A28: C c= A and
A29: z = union C by A7, A26, CANTOR_1:def 1;
consider w being set such that
A30: a in w and
A31: w in C by A27, A29, TARSKI:def 4;
take w = w; :: thesis: ( w in A & S₁[z,w] )
thus w in A by A28, A31; :: thesis: S₁[z,w]
thus S₁[z,w] by A29, A30, A31, ZFMISC_1:74; :: thesis: verum

end;

consider f being Function such that
A32: ( dom f = Z & rng f c= A ) and
A33: for z being set st z in Z holds
S₁[z,f . z] from FUNCT_1:sch 5(A25);
reconsider f = f as Element of Funcs (Z,A) by A32, FUNCT_2:def 2;
for z being set st z in Z holds
f . z c= z by A33;
then A34: meet (rng f) in G ;

now

thus rng f <> {} by A11; :: thesis: for y being set st y in rng f holds
a in y
let y be set ; :: thesis: ( y in rng f implies a in y )
assume y in rng f ; :: thesis: a in y
then ex z being set st
( z in Z & y = f . z ) by A32, FUNCT_1:def 3;
hence a in y by A33; :: thesis: verum

end;

then a in meet (rng f) by SETFAM_1:def 1;
hence a in union G by A34, TARSKI:def 4; :: thesis: verum

end;

hence y in UniCl (FinMeetCl A) by A13, CANTOR_1:def 1; :: thesis: verum

end;

end;

end;

hence x in UniCl (UniCl (FinMeetCl A)) by A6, CANTOR_1:def 1; :: thesis: verum

end;

FinMeetCl A c= FinMeetCl (UniCl A) by CANTOR_1:1, CANTOR_1:14;
then A35: UniCl (FinMeetCl A) c= UniCl (FinMeetCl (UniCl A)) by CANTOR_1:9;
UniCl (UniCl (FinMeetCl A)) = UniCl (FinMeetCl A) by Th15;
hence UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A) by A4, A35, XBOOLE_0:def 10; :: thesis: verum

end;

end;