let X be set ; :: thesis: for A being Subset-Family of X holds FinMeetCl A = FinMeetCl (FinMeetCl A)
let A be Subset-Family of X; :: thesis: FinMeetCl A = FinMeetCl (FinMeetCl A)
defpred S₁[ object , object ] means ex A being Subset-Family of X st
( $1 = Intersect A & A = $2 & A is finite );
thus FinMeetCl A c= FinMeetCl (FinMeetCl A) by Th4; :: according to XBOOLE_0:def 10 :: thesis: FinMeetCl (FinMeetCl A) c= FinMeetCl A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in FinMeetCl (FinMeetCl A) or x in FinMeetCl A )
assume A1: x in FinMeetCl (FinMeetCl A) ; :: thesis: x in FinMeetCl A
then reconsider x9 = x as Subset of X ;
consider Y being Subset-Family of X such that
A2: Y c= FinMeetCl A and
A3: Y is finite and
A4: x9 = Intersect Y by A1, Def3;
A5: for e being object st e in Y holds
ex u being object st
( u in bool A & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in Y implies ex u being object st
( u in bool A & S₁[e,u] ) )
assume A6: e in Y ; :: thesis: ex u being object st
( u in bool A & S₁[e,u] )
then reconsider e9 = e as Subset of X ;
consider Y being Subset-Family of X such that
A7: ( Y c= A & Y is finite & e9 = Intersect Y ) by A2, A6, Def3;
take Y ; :: thesis: ( Y in bool A & S₁[e,Y] )
thus ( Y in bool A & S₁[e,Y] ) by A7; :: thesis: verum

end;

consider f being Function of Y,(bool A) such that
A8: for e being object st e in Y holds
S₁[e,f . e] from FUNCT_2:sch 1(A5);
set fz = { (Intersect s) where s is Subset-Family of X : s in rng f } ;
A9: { (Intersect s) where s is Subset-Family of X : s in rng f } c= Y

proof

let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in { (Intersect s) where s is Subset-Family of X : s in rng f } or l in Y )
assume l in { (Intersect s) where s is Subset-Family of X : s in rng f } ; :: thesis: l in Y
then consider s being Subset-Family of X such that
A10: l = Intersect s and
A11: s in rng f ;
consider v being object such that
A12: v in dom f and
A13: s = f . v by A11, FUNCT_1:def 3;
v in Y by A12, FUNCT_2:def 1;
then S₁[v,f . v] by A8;
hence l in Y by A10, A12, A13, FUNCT_2:def 1; :: thesis: verum

end;

rng f c= bool A by RELAT_1:def 19;
then union (rng f) c= union (bool A) by ZFMISC_1:77;
then A14: union (rng f) c= A by ZFMISC_1:81;
then reconsider y = union (rng f) as Subset-Family of X by XBOOLE_1:1;
reconsider y = y as Subset-Family of X ;
Y c= { (Intersect s) where s is Subset-Family of X : s in rng f }

proof

let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in Y or l in { (Intersect s) where s is Subset-Family of X : s in rng f } )
assume A15: l in Y ; :: thesis: l in { (Intersect s) where s is Subset-Family of X : s in rng f }
then consider C being Subset-Family of X such that
A16: l = Intersect C and
A17: C = f . l and
C is finite by A8;
l in dom f by A15, FUNCT_2:def 1;
then C in rng f by A17, FUNCT_1:def 3;
hence l in { (Intersect s) where s is Subset-Family of X : s in rng f } by A16; :: thesis: verum

end;

then A18: Y = { (Intersect s) where s is Subset-Family of X : s in rng f } by A9;
A19: x = Intersect y

proof

per cases ( rng f <> {} or rng f = {} ) ;

suppose A20: rng f <> {} ; :: thesis: x = Intersect y

( rng f c= bool A & bool A c= bool (bool X) ) by RELAT_1:def 19, ZFMISC_1:67;
then reconsider GGG = rng f as non empty Subset-Family of (bool X) by A20, XBOOLE_1:1;
reconsider GGG = GGG as non empty Subset-Family of (bool X) ;
{ (Intersect s) where s is Subset-Family of X : s in rng f } = { (Intersect b) where b is Element of GGG : verum }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (Intersect b) where b is Element of GGG : verum } c= { (Intersect s) where s is Subset-Family of X : s in rng f }

let x be object ; :: thesis: ( x in { (Intersect s) where s is Subset-Family of X : s in rng f } implies x in { (Intersect b) where b is Element of GGG : verum } )
assume x in { (Intersect s) where s is Subset-Family of X : s in rng f } ; :: thesis: x in { (Intersect b) where b is Element of GGG : verum }
then ex s being Subset-Family of X st
( x = Intersect s & s in rng f ) ;
hence x in { (Intersect b) where b is Element of GGG : verum } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Intersect b) where b is Element of GGG : verum } or x in { (Intersect s) where s is Subset-Family of X : s in rng f } )
assume x in { (Intersect b) where b is Element of GGG : verum } ; :: thesis: x in { (Intersect s) where s is Subset-Family of X : s in rng f }
then ex s being Element of GGG st x = Intersect s ;
hence x in { (Intersect s) where s is Subset-Family of X : s in rng f } ; :: thesis: verum

end;

hence x = Intersect y by A4, A18, Th10; :: thesis: verum

end;

suppose A21: rng f = {} ; :: thesis: x = Intersect y

Y = dom f by FUNCT_2:def 1;
hence x = Intersect y by A4, A21, RELAT_1:38, RELAT_1:41, ZFMISC_1:2; :: thesis: verum

end;

end;

end;

for V being set st V in rng f holds
V is finite

proof

let V be set ; :: thesis: ( V in rng f implies V is finite )
assume V in rng f ; :: thesis: V is finite
then consider x being object such that
A22: x in dom f and
A23: V = f . x by FUNCT_1:def 3;
x in Y by A22, FUNCT_2:def 1;
then reconsider x = x as Subset of X ;
reconsider G = f . x as Subset-Family of X ;
x in Y by A22, FUNCT_2:def 1;
then S₁[x,G] by A8;
hence V is finite by A23; :: thesis: verum

end;

then union (rng f) is finite by A3, FINSET_1:7;
hence x in FinMeetCl A by A14, A19, Def3; :: thesis: verum