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: dom f = the carrier of S by FUNCT_2:def 1;
A4: for b being Element of S st {x,y} is_>=_than b holds
x >= b by YELLOW_0:8;
A5: x <= x ;
then A6: {x,y} is_>=_than x by A2, YELLOW_0:8;
then A7: 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 A8: ( 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 A2, A5, A8, TARSKI:def 2; :: thesis: verum

end;

then ( {x,y} is filtered & not {x,y} is empty ) ;
then A9: f preserves_inf_of {x,y} by A1;
x = inf {x,y} by A6, A4, YELLOW_0:31;
then inf (f .: {x,y}) = f . x by A7, A9;
then A10: f . x = inf {(f . x),(f . y)} by A3, FUNCT_1:60;
f .: {x,y} = {(f . x),(f . y)} by A3, FUNCT_1:60;
then ex_inf_of {(f . x),(f . y)},T by A7, A9;
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