let X be set ; :: thesis:
let A be Subset-Family of X; :: thesis:
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:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in FinMeetCl (FinMeetCl A) ; :: thesis:
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] )

let e be object ; :: thesis:
assume A6: e in Y ; :: thesis:
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:
thus ( Y in bool A & S₁[e,Y] ) by A7; :: thesis:

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

let l be object ; :: according to TARSKI:def 3 :: thesis:
assume l in { (Intersect s) where s is Subset-Family of X : s in rng f } ; :: thesis:
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:

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 }

let l be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: l in Y ; :: thesis:
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:

end;

( 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 }

let x be object ; :: thesis:
assume x in { (Intersect s) where s is Subset-Family of X : s in rng f } ; :: thesis:
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:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (Intersect b) where b is Element of GGG : verum } ; :: thesis:
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:

end;

end;

end;

let V be set ; :: thesis:
assume V in rng f ; :: thesis:
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:

end;