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 object ; :: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in UniCl (FinMeetCl A) )
reconsider yy = y as set by TARSKI:1;
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 object ; :: 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 = yy

proof

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

let a be object ; :: thesis: ( a in union G implies a in yy )
assume a in union G ; :: thesis: a in yy
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= yy

proof

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

now :: thesis: for d being set st d in Z holds
c in d

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 yy by A11, A12, SETFAM_1:def 1; :: thesis: verum

end;

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

end;

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

A25: now :: thesis: for z being object st z in Z holds
ex w being object st
( w in A & S₁[z,w] )

let z be object ; :: thesis: ( z in Z implies ex w being object st
( w in A & S₁[z,w] ) )
assume A26: z in Z ; :: thesis: ex w being object st
( w in A & S₁[z,w] )
reconsider zz = z as set by TARSKI:1;
A27: a in zz by A12, A24, SETFAM_1:def 1, A26;
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;
reconsider w = w as object ;
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 object st z in Z holds
S₁[z,f . z] from FUNCT_1:sch 6(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

proof

let z be set ; :: thesis: ( z in Z implies f . z c= z )
assume z in Z ; :: thesis: f . z c= z
then S₁[z,f . z] by A33;
hence f . z c= z ; :: thesis: verum

end;

then A34: meet (rng f) in G ;

now :: thesis: ( rng f <> {} & ( for y being set st y in rng f holds
a in y ) )

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 consider z being object such that
A35: ( z in Z & y = f . z ) by A32, FUNCT_1:def 3;
S₁[z,f . z] by A33, A35;
hence a in y by A35; :: 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 A36: 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, A36; :: thesis: verum

end;

end;