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

A5: now :: thesis: for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,S

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

end;

A6: now :: thesis: for Y being finite Subset of X st Y <> {} holds
"/\" (Y,S) in Z

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

end;

A7: for x being Element of S st x in Z holds
ex Y being finite Subset of X st
( ex_inf_of Y,S & x = "/\" (Y,S) ) by A4;
then A8: Z is filtered by A5, A6, Th56;
A9: ex_inf_of Z,S by A3, A5, A6, A7, Th58;
( Z = {} or Z <> {} ) ;
then A10: f preserves_inf_of Z by A1, A2, A8;
then A11: ex_inf_of f .: Z,T by A9;
A12: inf (f .: Z) = f . (inf Z) by A9, A10;
A13: inf Z = inf X by A3, A5, A6, A7, Th59;
X c= Z

proof

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

end;

then A16: f .: X c= f .: Z by RELAT_1:123;
A17: f .: Z is_>=_than f . (inf X) by A11, A12, A13, YELLOW_0:31;
A18: f .: X is_>=_than f . (inf X) by A16, A17;

A19: now :: thesis: for b being Element of T st f .: X is_>=_than b holds
f . (inf X) >= b

let b be Element of T; :: thesis: ( f .: X is_>=_than b implies f . (inf X) >= b )
assume A20: f .: X is_>=_than b ; :: thesis: f . (inf X) >= b
f .: Z is_>=_than b

proof

let a be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not a in f .: Z or b <= a )
assume a in f .: Z ; :: thesis: b <= a
then consider x being object such that
x in dom f and
A21: x in Z and
A22: a = f . x by FUNCT_1:def 6;
consider Y being finite Subset of X such that
A23: ex_inf_of Y,S and
A24: x = "/\" (Y,S) by A4, A21;
reconsider Y = Y as Subset of S by XBOOLE_1:1;
A25: f .: Y c= f .: X by RELAT_1:123;
A26: f preserves_inf_of Y by A1;
A27: b is_<=_than f .: Y by A20, A25;
A28: a = "/\" ((f .: Y),T) by A22, A23, A24, A26;
ex_inf_of f .: Y,T by A23, A26;
hence b <= a by A27, A28, YELLOW_0:def 10; :: thesis: verum

end;

hence f . (inf X) >= b by A11, A12, A13, YELLOW_0:31; :: thesis: verum

end;

hence ex_inf_of f .: X,T by A18, YELLOW_0:16; :: thesis: inf (f .: X) = f . (inf X)
hence inf (f .: X) = f . (inf X) by A18, A19, YELLOW_0:def 10; :: thesis: verum