let L be with_suprema Poset; :: thesis: for f being Function of L,L st f is directed-sups-preserving holds
f is monotone
let f be Function of L,L; :: 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 L; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of L holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ ) )
assume A2: x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ )
A3: y = y "\/" x by A2, YELLOW_0:24;
for a, b being Element of L st a in {x,y} & b in {x,y} holds
ex z being Element of L st
( z in {x,y} & a <= z & b <= z )

proof

let a, b be Element of L; :: thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of L st
( z in {x,y} & a <= z & b <= z ) )
assume A4: ( a in {x,y} & b in {x,y} ) ; :: thesis: ex z being Element of L 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, A4, TARSKI:def 2; :: thesis: verum

end;

then ( {x,y} is directed & not {x,y} is empty ) ;
then A5: f preserves_sup_of {x,y} by A1;
A6: dom f = the carrier of L by FUNCT_2:def 1;
y <= y ;
then A7: {x,y} is_<=_than y by A2, YELLOW_0:8;
for b being Element of L st {x,y} is_<=_than b holds
y <= b by YELLOW_0:8;
then ex_sup_of {x,y},L by A7, YELLOW_0:30;
then sup (f .: {x,y}) = f . (sup {x,y}) by A5
.= f . y by A3, YELLOW_0:41 ;
then A8: f . y = sup {(f . x),(f . y)} by A6, FUNCT_1:60
.= (f . y) "\/" (f . x) by YELLOW_0:41 ;
let afx, bfy be Element of L; :: thesis: ( not afx = f . x or not bfy = f . y or afx <= bfy )
assume ( afx = f . x & bfy = f . y ) ; :: thesis: afx <= bfy
hence afx <= bfy by A8, YELLOW_0:22; :: thesis: verum