let X be non empty set ; :: thesis: for B being non empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
FinMeetCl B c= UniCl B

let B be non empty Subset-Family of X; :: thesis: ( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B implies FinMeetCl B c= UniCl B )
assume that
A1: for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB and
A2: X = union B ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in FinMeetCl B or x in UniCl B )
assume A3: x in FinMeetCl B ; :: thesis: x in UniCl B
then reconsider x0 = x as Subset of X ;
consider Y being Subset-Family of X such that
A4: Y c= B and
A5: Y is finite and
A6: x0 = Intersect Y by ;
defpred S1[ Nat] means for Y being Subset-Family of X
for x being Subset of X st Y c= B & card Y = \$1 & x = Intersect Y holds
x in UniCl B;
A7: S1[ 0 ]
proof
let Y be Subset-Family of X; :: thesis: for x being Subset of X st Y c= B & card Y = 0 & x = Intersect Y holds
x in UniCl B

let x be Subset of X; :: thesis: ( Y c= B & card Y = 0 & x = Intersect Y implies x in UniCl B )
assume that
Y c= B and
A8: card Y = 0 and
A9: x = Intersect Y ; :: thesis: x in UniCl B
Y = {} by A8;
then A10: x = X by ;
reconsider x0 = x as set ;
thus x in UniCl B by ; :: thesis: verum
end;
A11: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A12: S1[k] ; :: thesis: S1[k + 1]
let Y be Subset-Family of X; :: thesis: for x being Subset of X st Y c= B & card Y = k + 1 & x = Intersect Y holds
x in UniCl B

let x be Subset of X; :: thesis: ( Y c= B & card Y = k + 1 & x = Intersect Y implies x in UniCl B )
assume that
A13: Y c= B and
A14: card Y = k + 1 and
A15: x = Intersect Y ; :: thesis: x in UniCl B
Y is finite set by A14;
then consider x1 being Element of Y, C being Subset of Y such that
A16: Y = C \/ {x1} and
A17: card C = k by ;
A18: ( C c= B & card C = k ) by ;
B c= bool X ;
then C c= bool X by A13;
then reconsider C0 = C as Subset-Family of X ;
per cases ( C = {} or C <> {} ) ;
suppose A19: C = {} ; :: thesis: x in UniCl B
meet {x1} = x1 by SETFAM_1:10;
then A20: Intersect Y = x1 by ;
then x1 in bool X ;
then {x1} c= bool X by TARSKI:def 1;
then reconsider B0 = {x1} as Subset-Family of X ;
x1 in Y by A16;
then A21: ( {x1} c= Y & Y c= B ) by ;
( x in B & B0 c= B & x = union B0 ) by A16, A21, A15, A20;
hence x in UniCl B by CANTOR_1:def 1; :: thesis: verum
end;
suppose A22: C <> {} ; :: thesis: x in UniCl B
then meet (C \/ {x1}) = (meet C) /\ (meet {x1}) by SETFAM_1:9;
then A23: meet Y = (meet C) /\ x1 by ;
meet Y = Intersect Y by ;
then A24: Intersect Y = () /\ x1 by ;
Intersect Y in UniCl B
proof
Intersect C0 in UniCl B by ;
then consider Y2 being Subset-Family of X such that
A25: Y2 c= B and
A26: Intersect C0 = union Y2 by CANTOR_1:def 1;
per cases ( Y2 is empty or not Y2 is empty ) ;
suppose A27: Y2 is empty ; :: thesis:
{} c= X ;
then reconsider x0 = {} as Subset of X ;
A28: ( {} c= bool X & {} c= B & {} = union {} ) by ZFMISC_1:2;
then reconsider S = {} as Subset-Family of X ;
thus Intersect Y in UniCl B by ; :: thesis: verum
end;
suppose A29: not Y2 is empty ; :: thesis:
set Y3 = { (y /\ x1) where y is Element of Y2 : verum } ;
{ (y /\ x1) where y is Element of Y2 : verum } c= bool X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (y /\ x1) where y is Element of Y2 : verum } or x in bool X )
assume A30: x in { (y /\ x1) where y is Element of Y2 : verum } ; :: thesis: x in bool X
then reconsider x = x as Element of { (y /\ x1) where y is Element of Y2 : verum } ;
consider y being Element of Y2 such that
A31: x = y /\ x1 by A30;
A32: x c= x1 by ;
( x1 in Y & Y c= bool X ) by A16;
then x1 c= X ;
then x c= X by A32;
hence x in bool X ; :: thesis: verum
end;
then reconsider Y3 = { (y /\ x1) where y is Element of Y2 : verum } as Subset-Family of X ;
A33: union Y3 = (union Y2) /\ x1
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (union Y2) /\ x1 c= union Y3
let x be object ; :: thesis: ( x in union Y3 implies x in (union Y2) /\ x1 )
assume A34: x in union Y3 ; :: thesis: x in (union Y2) /\ x1
consider a1 being set such that
A35: x in a1 and
A36: a1 in Y3 by ;
consider x2 being Element of Y2 such that
A37: a1 = x2 /\ x1 by A36;
( x in a1 & a1 c= x2 & a1 c= x1 ) by ;
then ( x in union Y2 & x in x1 ) by ;
hence x in (union Y2) /\ x1 by XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union Y2) /\ x1 or x in union Y3 )
assume x in (union Y2) /\ x1 ; :: thesis: x in union Y3
then A38: ( x in union Y2 & x in x1 ) by XBOOLE_0:def 4;
then consider a being set such that
A39: x in a and
A40: a in Y2 by TARSKI:def 4;
reconsider a = a as Element of Y2 by A40;
A41: x in a /\ x1 by ;
a /\ x1 in Y3 ;
hence x in union Y3 by ; :: thesis: verum
end;
A42: Intersect Y = union Y3
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:
let t be object ; :: thesis: ( t in Intersect Y implies t in union Y3 )
assume t in Intersect Y ; :: thesis: t in union Y3
then A43: ( t in union Y2 & t in x1 ) by ;
then consider t0 being set such that
A44: t in t0 and
A45: t0 in Y2 by TARSKI:def 4;
A46: t in t0 /\ x1 by ;
t0 /\ x1 in Y3 by A45;
hence t in union Y3 by ; :: thesis: verum
end;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in union Y3 or t in Intersect Y )
assume t in union Y3 ; :: thesis:
then ( t in union Y2 & t in x1 ) by ;
then ( t in meet C0 & t in x1 ) by ;
then t in (meet C0) /\ x1 by XBOOLE_0:def 4;
hence t in Intersect Y by ; :: thesis: verum
end;
Y3 c= UniCl B
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Y3 or t in UniCl B )
assume t in Y3 ; :: thesis: t in UniCl B
then consider a being Element of Y2 such that
A47: t = a /\ x1 ;
reconsider a2 = a as Element of B by ;
reconsider x2 = x1 as Element of B by ;
consider BP being Subset of B such that
A48: a2 /\ x2 = union BP by A1;
reconsider ax = a2 /\ x2 as Subset of X ;
( BP c= B & B c= bool X ) ;
then A49: BP c= bool X ;
thus t in UniCl B by ; :: thesis: verum
end;
then Intersect Y in UniCl () by ;
hence Intersect Y in UniCl B by YELLOW_9:15; :: thesis: verum
end;
end;
end;
hence x in UniCl B by A15; :: thesis: verum
end;
end;
end;
A50: for k being Nat holds S1[k] from NAT_1:sch 2(A7, A11);
reconsider CY = card Y as Nat by A5;
S1[CY] by A50;
hence x in UniCl B by A4, A6; :: thesis: verum