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 A = {} ; :: thesis: UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)

then ( FinMeetCl A = {X} & UniCl A = {{} } ) by Th16, Th17;
then ( FinMeetCl (UniCl A) = {{} ,X} & UniCl (FinMeetCl A) = {X,{} } ) by Th11;
hence UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A) by 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 ;
A1: 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
A2: ( Y c= FinMeetCl (UniCl A) & 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
A3: ( Z c= UniCl A & Z is finite & y = Intersect Z ) by A2, CANTOR_1:def 4;

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

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

then y = X by A3, SETFAM_1:def 10;
then ( y in FinMeetCl A & FinMeetCl A c= UniCl (FinMeetCl A) ) by CANTOR_1:1, CANTOR_1:8;
hence y in UniCl (FinMeetCl A) ; :: thesis: verum

end;

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

then A5: y = meet Z by A3, SETFAM_1:def 10;
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 } ;
A6: { (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
A7: ( a = meet (rng f) & ( for z being set st z in Z holds
f . z c= z ) ) ;
Funcs Z,A is FUNCTION_DOMAIN of Z,A ;
then f is Function of Z,A by FUNCT_2:def 13;
then A8: ( dom f = Z & rng f c= A ) by FUNCT_2:def 1, RELAT_1:def 19;
then reconsider B = rng f as Subset-Family of X by XBOOLE_1:1;
reconsider B = B as Subset-Family of X ;
B <> {} by A4, A8, RELAT_1:65;
then ( Intersect B = a & B is finite ) by A3, A7, A8, FINSET_1:26, SETFAM_1:def 10;
hence a in FinMeetCl A by A8, CANTOR_1:def 4; :: 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
A9: ( a in b & b in G ) by TARSKI:def 4;
consider f being Element of Funcs Z,A such that
A10: ( b = meet (rng f) & ( for z being set st z in Z holds
f . z c= z ) ) by A9;
Funcs Z,A is FUNCTION_DOMAIN of Z,A ;
then f is Function of Z,A by FUNCT_2:def 13;
then A11: ( dom f = Z & rng f c= A ) by FUNCT_2:def 1, RELAT_1:def 19;
then 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 A12: c in b ; :: thesis: c in y

now

let d be set ; :: thesis: ( d in Z implies c in d )
assume A13: d in Z ; :: thesis: c in d
then f . d in B by A11, FUNCT_1:def 5;
then b c= f . d by A10, SETFAM_1:4;
then ( f . d c= d & c in f . d ) by A10, A12, A13;
hence c in d ; :: thesis: verum

end;

hence c in y by A4, A5, SETFAM_1:def 1; :: thesis: verum

end;

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

end;

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

A15: now

let z be set ; :: thesis: ( z in Z implies ex w being set st
( w in A & S₁[z,w] ) )
assume A16: z in Z ; :: thesis: ex w being set st
( w in A & S₁[z,w] )
then A17: ( a in z & z in UniCl A ) by A3, A5, A14, SETFAM_1:def 1;
consider C being Subset-Family of X such that
A18: ( C c= A & z = union C ) by A3, A16, CANTOR_1:def 1;
consider w being set such that
A19: ( a in w & w in C ) by A17, A18, TARSKI:def 4;
take w = w; :: thesis: ( w in A & S₁[z,w] )
thus w in A by A18, A19; :: thesis: S₁[z,w]
thus S₁[z,w] by A18, A19, ZFMISC_1:92; :: thesis: verum

end;

consider f being Function such that
A20: ( dom f = Z & rng f c= A ) and
A21: for z being set st z in Z holds
S₁[z,f . z] from WELLORD2:sch 1(A15);
reconsider f = f as Element of Funcs Z,A by A20, FUNCT_2:def 2;
for z being set st z in Z holds
f . z c= z by A21;
then A22: meet (rng f) in G ;

now

thus rng f <> {} by A4, A20, RELAT_1:65; :: 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 A20, FUNCT_1:def 5;
hence a in y by A21; :: thesis: verum

end;

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

end;

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

end;

end;

end;

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

end;

FinMeetCl A c= FinMeetCl (UniCl A) by CANTOR_1:1, CANTOR_1:16;
then ( UniCl (FinMeetCl A) c= UniCl (FinMeetCl (UniCl A)) & UniCl (UniCl (FinMeetCl A)) = UniCl (FinMeetCl A) ) by Th15, CANTOR_1:9;
hence UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A) by A1, XBOOLE_0:def 10; :: thesis: verum

end;

end;