consider x being Element of T;
take f = S --> x; :: thesis: ( f is directed-sups-preserving & f is monotone )
thus f is directed-sups-preserving :: thesis: f is monotone
proof
let X be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or f preserves_sup_of X )
assume A1: ( not X is empty & X is directed ) ; :: thesis: f preserves_sup_of X
A2: f .: X = {x}
proof
consider a being Element of X;
thus f .: X c= {x} by FUNCOP_1:96; :: according to XBOOLE_0:def 10 :: thesis: {x} c= f .: X
A3: dom f = the carrier of S by FUNCOP_1:19;
A4: a in X by A1;
then f . a = x by FUNCOP_1:13;
then x in f .: X by A4, A3, FUNCT_1:def 12;
hence {x} c= f .: X by ZFMISC_1:37; :: thesis: verum
end;
assume ex_sup_of X,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: X,T & "\/" ((f .: X),T) = f . ("\/" (X,S)) )
thus ex_sup_of f .: X,T by A2, YELLOW_0:38; :: thesis: "\/" ((f .: X),T) = f . ("\/" (X,S))
thus sup (f .: X) = x by A2, YELLOW_0:39
.= f . (sup X) by FUNCOP_1:13 ; :: thesis: verum
end;
let a, b be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not a <= b or f . a <= f . b )
A5: x <= x ;
f . a = x by FUNCOP_1:13;
hence ( not a <= b or f . a <= f . b ) by A5, FUNCOP_1:13; :: thesis: verum