let S, T be non empty reflexive antisymmetric RelStr ; :: thesis: for f being Function of S,T st f is filtered-infs-preserving holds
f is monotone
let f be Function of S,T; :: thesis: ( f is filtered-infs-preserving implies f is monotone )
assume A1: f is filtered-infs-preserving ; :: thesis: f is monotone
let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or f . x <= f . y )
assume A2: x <= y ; :: thesis: f . x <= f . y
A3: ( x <= y & x <= x ) by A2;
then A4: {x,y} is_>=_than x by YELLOW_0:8;
for b being Element of S st {x,y} is_>=_than b holds
x >= b by YELLOW_0:8;
then A5: ( x = inf {x,y} & ex_inf_of {x,y},S ) by A4, YELLOW_0:31;
for a, b being Element of S st a in {x,y} & b in {x,y} holds
ex z being Element of S st
( z in {x,y} & a >= z & b >= z )

proof

let a, b be Element of S; :: thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of S st
( z in {x,y} & a >= z & b >= z ) )
assume A6: ( a in {x,y} & b in {x,y} ) ; :: thesis: ex z being Element of S st
( z in {x,y} & a >= z & b >= z )
take x ; :: thesis: ( x in {x,y} & a >= x & b >= x )
thus x in {x,y} by TARSKI:def 2; :: thesis: ( a >= x & b >= x )
thus ( a >= x & b >= x ) by A3, A6, TARSKI:def 2; :: thesis: verum

end;

then ( {x,y} is filtered & not {x,y} is empty ) by WAYBEL_0:def 2;
then A7: f preserves_inf_of {x,y} by A1, WAYBEL_0:def 36;
then A8: inf (f .: {x,y}) = f . x by A5, WAYBEL_0:def 30;
A9: dom f = the carrier of S by FUNCT_2:def 1;
then A10: f . x = inf {(f . x),(f . y)} by A8, FUNCT_1:118;
f .: {x,y} = {(f . x),(f . y)} by A9, FUNCT_1:118;
then ex_inf_of {(f . x),(f . y)},T by A5, A7, WAYBEL_0:def 30;
then {(f . x),(f . y)} is_>=_than f . x by A10, YELLOW_0:def 10;
hence f . x <= f . y by YELLOW_0:8; :: thesis: verum