let S, T be non empty reflexive antisymmetric RelStr ; :: thesis: for f being Function of S,T st f is directed-sups-preserving holds

f is monotone

let f be Function of S,T; :: thesis: ( f is directed-sups-preserving implies f is monotone )

assume A1: f is directed-sups-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

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 )

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; :: thesis: verum

f is monotone

let f be Function of S,T; :: thesis: ( f is directed-sups-preserving implies f is monotone )

assume A1: f is directed-sups-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

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

then
( {x,y} is directed & not {x,y} is empty )
;
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 that

A7: a in {x,y} and

A8: b in {x,y} ; :: thesis: ex z being Element of S st

( z in {x,y} & a <= z & b <= z )

take y ; :: thesis: ( y in {x,y} & a <= y & b <= y )

thus y in {x,y} by TARSKI:def 2; :: thesis: ( a <= y & b <= y )

thus ( a <= y & b <= y ) by A2, A7, A8, TARSKI:def 2; :: thesis: verum

end;( z in {x,y} & a <= z & b <= z ) )

assume that

A7: a in {x,y} and

A8: b in {x,y} ; :: thesis: ex z being Element of S st

( z in {x,y} & a <= z & b <= z )

take y ; :: thesis: ( y in {x,y} & a <= y & b <= y )

thus y in {x,y} by TARSKI:def 2; :: thesis: ( a <= y & b <= y )

thus ( a <= y & b <= y ) by A2, A7, A8, TARSKI:def 2; :: thesis: verum

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; :: thesis: verum