let S, T be non empty reflexive antisymmetric RelStr ; for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
let f be Function of S,T; ( f is directed-sups-preserving implies f is monotone )
assume A1:
f is directed-sups-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
y <= y
;
then A3:
{x,y} is_<=_than y
by A2, YELLOW_0:8;
A4:
for b being Element of S st {x,y} is_<=_than b holds
y <= b
by YELLOW_0:8;
then A5:
y = sup {x,y}
by A3, YELLOW_0:30;
A6:
ex_sup_of {x,y},S
by A3, A4, YELLOW_0:30;
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 that A7:
a in {x,y}
and A8:
b in {x,y}
;
ex z being Element of S st
( z in {x,y} & a <= z & b <= z )
take
y
;
( y in {x,y} & a <= y & b <= y )
thus
y in {x,y}
by TARSKI:def 2;
( a <= y & b <= y )
thus
(
a <= y &
b <= y )
by A2, A7, A8, TARSKI:def 2;
verum
end;
then
( {x,y} is directed & not {x,y} is empty )
;
then A9:
f preserves_sup_of {x,y}
by A1;
then A10:
sup (f .: {x,y}) = f . y
by A5, A6;
A11:
dom f = the carrier of S
by FUNCT_2:def 1;
then A12:
f . y = sup {(f . x),(f . y)}
by A10, FUNCT_1:60;
f .: {x,y} = {(f . x),(f . y)}
by A11, FUNCT_1:60;
then
ex_sup_of {(f . x),(f . y)},T
by A6, A9;
then
{(f . x),(f . y)} is_<=_than f . y
by A12, YELLOW_0:def 9;
hence
f . x <= f . y
by YELLOW_0:8; verum