let S, T be Semilattice; :: thesis:
let f be Function of S,T; :: thesis:
assume that
A1: f is meet-preserving and
A2: for X being non empty filtered Subset of S holds f preserves_inf_of X ; :: thesis:
let X be non empty Subset of S; :: thesis:
assume A3: ex_inf_of X,S ; :: according to WAYBEL_0:def 30 :: thesis:
defpred S₁[ set ] means ex Y being non empty finite Subset of X st
( ex_inf_of Y,S & $1 = "/\" Y,S );
consider Z being set such that
A4: for x being set holds
( x in Z iff ( x in the carrier of S & S₁[x] ) ) from XBOOLE_0:sch 1();
consider a being Element of X;
reconsider a' = a as Element of S ;
A5: ( ex_inf_of {a},S & inf {a'} = a & {a} c= X ) by YELLOW_0:38, YELLOW_0:39;
Z c= the carrier of S

let x be set ; :: according to TARSKI:def 3 :: thesis:
thus ( not x in Z or x in the carrier of S ) by A4; :: thesis:

end;

then reconsider Z = Z as non empty Subset of S by A4, A5;

A6: now

let Y be finite Subset of X; :: thesis:
Y is Subset of S by XBOOLE_1:1;
hence ( Y <> {} implies ex_inf_of Y,S ) by YELLOW_0:55; :: thesis:

end;

A7: now

let Y be finite Subset of X; :: thesis:
reconsider Y' = Y as Subset of S by XBOOLE_1:1;
assume A8: Y <> {} ; :: thesis:
then ex_inf_of Y',S by YELLOW_0:55;
hence "/\" Y,S in Z by A4, A8; :: thesis:

end;

now

let x be Element of S; :: thesis:
assume x in Z ; :: thesis:
then ex Y being non empty finite Subset of X st
( ex_inf_of Y,S & x = "/\" Y,S ) by A4;
hence ex Y being finite Subset of X st
( ex_inf_of Y,S & x = "/\" Y,S ) ; :: thesis:

end;

then A9: ( Z is filtered & ex_inf_of Z,S & inf Z = inf X & Z <> {} ) by A3, A6, A7, WAYBEL_0:56, WAYBEL_0:58, WAYBEL_0:59;
then f preserves_inf_of Z by A2;
then A10: ( ex_inf_of f .: Z,T & inf (f .: Z) = f . (inf Z) & inf Z = inf X ) by A9, WAYBEL_0:def 30;
X c= Z

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: x in X ; :: thesis:
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:37;
reconsider x = x as Element of S by A11;
Y is Subset of S by XBOOLE_1:1;
then ( ex_inf_of Y,S & x = "/\" Y,S ) by YELLOW_0:39, YELLOW_0:55;
hence x in Z by A4; :: thesis:

end;

then A12: f .: X c= f .: Z by RELAT_1:156;
A13: f .: Z is_>=_than f . (inf X) by A10, YELLOW_0:31;
A14: f .: X is_>=_than f . (inf X)

let x be Element of T; :: according to LATTICE3:def 8 :: thesis:
assume x in f .: X ; :: thesis:
hence f . (inf X) <= x by A12, A13, LATTICE3:def 8; :: thesis:

end;

A15: now

let b be Element of T; :: thesis:
assume A16: f .: X is_>=_than b ; :: thesis:
f .: Z is_>=_than b

let a be Element of T; :: according to LATTICE3:def 8 :: thesis:
assume a in f .: Z ; :: thesis:
then consider x being set such that
A17: ( x in dom f & x in Z & a = f . x ) by FUNCT_1:def 12;
consider Y being non empty finite Subset of X such that
A18: ( ex_inf_of Y,S & x = "/\" Y,S ) by A4, A17;
reconsider Y = Y as Subset of S by XBOOLE_1:1;
( f .: Y c= f .: X & f preserves_inf_of Y ) by A1, Th2, RELAT_1:156;
then ( b is_<=_than f .: Y & a = "/\" (f .: Y),T & ex_inf_of f .: Y,T ) by A16, A17, A18, WAYBEL_0:def 30, YELLOW_0:9;
hence b <= a by YELLOW_0:def 10; :: thesis:

end;

hence f . (inf X) >= b by A10, YELLOW_0:31; :: thesis:

end;

hence ex_inf_of f .: X,T by A14, YELLOW_0:16; :: thesis:
hence inf (f .: X) = f . (inf X) by A14, A15, YELLOW_0:def 10; :: thesis: