let S, T be non empty reflexive antisymmetric RelStr ; for f being Function of S,T st f is filtered-infs-preserving holds
f is monotone
let f be Function of S,T; ( f is filtered-infs-preserving implies f is monotone )
assume A1:
f is filtered-infs-preserving
; f is monotone
let x, y be Element of S; WAYBEL_1:def 2 ( not x <= y or f . x <= f . y )
assume A2:
x <= y
; 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;
( 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} )
;
ex z being Element of S st
( z in {x,y} & a >= z & b >= z )
take
x
;
( x in {x,y} & a >= x & b >= x )
thus
x in {x,y}
by TARSKI:def 2;
( a >= x & b >= x )
thus
(
a >= x &
b >= x )
by A2, A5, A8, TARSKI:def 2;
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; verum