let S, T be non empty Poset; :: thesis: for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is filtered-infs-preserving
let f be Function of S,T; :: thesis: ( ( for X being Filter of S holds f preserves_inf_of X ) implies f is filtered-infs-preserving )
assume A1: for X being Filter of S holds f preserves_inf_of X ; :: thesis: f is filtered-infs-preserving
let X be Subset of S; :: according to WAYBEL_0:def 36 :: thesis: ( not X is empty & X is filtered implies f preserves_inf_of X )
assume that
A2: ( not X is empty & X is filtered ) and
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) )
reconsider Y = X as non empty filtered Subset of S by A2;
uparrow Y is Filter of S ;
then A4: f preserves_inf_of uparrow X by A1;
A5: ex_inf_of uparrow X,S by A3, Th37;
then A6: ex_inf_of f .: (uparrow X),T by A4;
A7: inf (f .: (uparrow X)) = f . (inf (uparrow X)) by A4, A5;
A8: inf (uparrow X) = inf X by A3, Th38;
A9: f .: X c= f .: (uparrow X) by Th16, RELAT_1:123;
A10: f .: (uparrow X) is_>=_than f . (inf X) by A6, A7, A8, YELLOW_0:31;
A11: f .: X is_>=_than f . (inf X) by A9, A10;

A12: 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 A13: f .: X is_>=_than b ; :: thesis: f . (inf X) >= b
f .: (uparrow X) is_>=_than b

proof

let a be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not a in f .: (uparrow X) or b <= a )
assume a in f .: (uparrow X) ; :: thesis: b <= a
then consider x being object such that
x in dom f and
A14: x in uparrow X and
A15: a = f . x by FUNCT_1:def 6;
uparrow X = { z where z is Element of S : ex y being Element of S st
( z >= y & y in X ) } by Th15;
then consider z being Element of S such that
A16: x = z and
A17: ex y being Element of S st
( z >= y & y in X ) by A14;
consider y being Element of S such that
A18: z >= y and
A19: y in X by A17;
A20: f is monotone by A1, Th69;
A21: f . y in f .: X by A19, FUNCT_2:35;
A22: f . z >= f . y by A18, A20;
f . y >= b by A13, A21;
hence b <= a by A15, A16, A22, ORDERS_2:3; :: thesis: verum

end;

hence f . (inf X) >= b by A6, A7, A8, YELLOW_0:31; :: thesis: verum

end;

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