set x = the Element of T;
take f = S --> the Element of T; :: 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 = { the Element of T}
proof
set a = the Element of X;
thus f .: X c= { the Element of T} by FUNCOP_1:81; :: according to XBOOLE_0:def 10 :: thesis: { the Element of T} c= f .: X
A3: dom f = the carrier of S ;
A4: the Element of X in X by A1;
then f . the Element of X = the Element of T by FUNCOP_1:7;
then the Element of T in f .: X by A4, A3, FUNCT_1:def 6;
hence { the Element of T} c= f .: X by ZFMISC_1:31; :: 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) = the Element of T by A2, YELLOW_0:39
.= f . (sup X) ; :: 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: the Element of T <= the Element of T ;
thus ( not a <= b or f . a <= f . b ) by A5; :: thesis: verum