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 ( f preserves_inf_of uparrow X & ex_inf_of uparrow X,S ) by A1, A3, Th37;
then A4: ( ex_inf_of f .: (uparrow X),T & inf (f .: (uparrow X)) = f . (inf (uparrow X)) & inf (uparrow X) = inf X ) by A3, Def30, Th38;
X c= uparrow X by Th16;
then A5: f .: X c= f .: (uparrow X) by RELAT_1:156;
A6: f .: (uparrow X) is_>=_than f . (inf X) by A4, YELLOW_0:31;
A7: f .: X is_>=_than f . (inf X)

proof

let x be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not x in f .: X or f . (inf X) <= x )
assume x in f .: X ; :: thesis: f . (inf X) <= x
hence f . (inf X) <= x by A5, A6, LATTICE3:def 8; :: thesis: verum

end;

A8: now

let b be Element of T; :: thesis: ( f .: X is_>=_than b implies f . (inf X) >= b )
assume A9: 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 set such that
A10: ( x in dom f & x in uparrow X & a = f . x ) by FUNCT_1:def 12;
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
A11: ( x = z & ex y being Element of S st
( z >= y & y in X ) ) by A10;
consider y being Element of S such that
A12: ( z >= y & y in X ) by A11;
( f is monotone & f . y in f .: X ) by A1, A12, Th69, FUNCT_2:43;
then ( f . z >= f . y & f . y >= b ) by A9, A12, LATTICE3:def 8, ORDERS_3:def 5;
hence b <= a by A10, A11, ORDERS_2:26; :: thesis: verum

end;

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

end;

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