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: FinMeetCl B c= UniCl B
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 A3, CANTOR_1:def 3;
defpred S₁[ 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: S₁[ 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 A9, SETFAM_1:def 9;
reconsider x0 = x as set ;
thus x in UniCl B by A2, A10, CANTOR_1:def 1; :: thesis: verum

end;

A11: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: S₁[k] ; :: thesis: S₁[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 A14, PRE_CIRC:24;
A18: ( C c= B & card C = k ) by A13, A17;
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 A19, A16, SETFAM_1:def 9;
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 A13, TARSKI:def 1;
( 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 A16, SETFAM_1:10;
meet Y = Intersect Y by A16, SETFAM_1:def 9;
then A24: Intersect Y = (Intersect C0) /\ x1 by A22, A23, SETFAM_1:def 9;
Intersect Y in UniCl B

proof

Intersect C0 in UniCl B by A18, A12;
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: Intersect Y in UniCl B

{} 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 A27, A24, A26, A28, CANTOR_1:def 1; :: thesis: verum

end;

suppose A29: not Y2 is empty ; :: thesis: Intersect Y in UniCl B

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 A31, XBOOLE_1:17;
( 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 A34, TARSKI:def 4;
consider x2 being Element of Y2 such that
A37: a1 = x2 /\ x1 by A36;
( x in a1 & a1 c= x2 & a1 c= x1 ) by A35, A37, XBOOLE_1:17;
then ( x in union Y2 & x in x1 ) by A29, TARSKI:def 4;
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 A38, A39, XBOOLE_0:def 4;
a /\ x1 in Y3 ;
hence x in union Y3 by A41, TARSKI:def 4; :: thesis: verum

end;

A42: Intersect Y = union Y3

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union Y3 c= Intersect Y

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 A24, A26, XBOOLE_0:def 4;
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 A43, A44, XBOOLE_0:def 4;
t0 /\ x1 in Y3 by A45;
hence t in union Y3 by A46, TARSKI:def 4; :: 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: t in Intersect Y
then ( t in union Y2 & t in x1 ) by A33, XBOOLE_0:def 4;
then ( t in meet C0 & t in x1 ) by A26, A22, SETFAM_1:def 9;
then t in (meet C0) /\ x1 by XBOOLE_0:def 4;
hence t in Intersect Y by A23, A16, SETFAM_1:def 9; :: 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 A29, A25;
reconsider x2 = x1 as Element of B by A13, A16;
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 A47, A48, A49, CANTOR_1:def 1; :: thesis: verum

end;

then Intersect Y in UniCl (UniCl B) by A42, CANTOR_1:def 1;
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 S₁[k] from NAT_1:sch 2(A7, A11);
reconsider CY = card Y as Nat by A5;
S₁[CY] by A50;
hence x in UniCl B by A4, A6; :: thesis: verum