reconsider f = the carrier of S --> (Top T) as Function of the carrier of S, the carrier of T ;
reconsider f = f as Function of S,T ;
take f ; :: thesis: ( f is directed-sups-preserving & f is infs-preserving )

now :: thesis: for X being Subset of S st not X is empty & X is directed holds
f preserves_sup_of X

let X be Subset of S; :: thesis: ( not X is empty & X is directed implies f preserves_sup_of X )
assume A1: ( not X is empty & X is directed ) ; :: thesis: f preserves_sup_of X

now :: thesis: ( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) )

assume ex_sup_of X,S ; :: thesis: ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) )
rng f = {(Top T)} by FUNCOP_1:8;
then A2: f .: X c= {(Top T)} by RELAT_1:111;

now :: thesis: for x, y being Element of S st x <= y holds
f . x <= f . y

let x, y be Element of S; :: thesis: ( x <= y implies f . x <= f . y )
assume x <= y ; :: thesis: f . x <= f . y
f . x = Top T by FUNCOP_1:7
.= f . y by FUNCOP_1:7 ;
hence f . x <= f . y ; :: thesis: verum

end;

then f is monotone by WAYBEL_1:def 2;
then A3: f .: X is non empty finite directed Subset of T by A1, A2, YELLOW_2:15;
hence ex_sup_of f .: X,T by WAYBEL_0:75; :: thesis: sup (f .: X) = f . (sup X)
sup (f .: X) in f .: X by A3, WAYBEL_3:16;
then sup (f .: X) = Top T by A2, TARSKI:def 1;
hence sup (f .: X) = f . (sup X) by FUNCOP_1:7; :: thesis: verum

end;

hence f preserves_sup_of X by WAYBEL_0:def 31; :: thesis: verum

end;

hence f is directed-sups-preserving by WAYBEL_0:def 37; :: thesis: f is infs-preserving

now :: thesis: for X being Subset of S holds f preserves_inf_of X

let X be Subset of S; :: thesis: f preserves_inf_of X

now :: thesis: ( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) )

assume ex_inf_of X,S ; :: thesis: ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) )
thus ex_inf_of f .: X,T by YELLOW_0:17; :: thesis: inf (f .: X) = f . (inf X)
rng f = {(Top T)} by FUNCOP_1:8;
then A4: f .: X is Subset of {(Top T)} by RELAT_1:111;

now :: thesis: inf (f .: X) = f . (inf X)

per cases ( f .: X = {} or f .: X <> {} ) ;

suppose f .: X = {} ; :: thesis: inf (f .: X) = f . (inf X)

hence inf (f .: X) = Top T by YELLOW_0:def 12
.= f . (inf X) by FUNCOP_1:7 ;
:: thesis: verum

end;

suppose f .: X <> {} ; :: thesis: inf (f .: X) = f . (inf X)

then f .: X = {(Top T)} by A4, ZFMISC_1:33;
hence inf (f .: X) = Top T by YELLOW_0:39
.= f . (inf X) by FUNCOP_1:7 ;
:: thesis: verum

end;

end;

end;

hence inf (f .: X) = f . (inf X) ; :: thesis: verum

end;

hence f preserves_inf_of X by WAYBEL_0:def 30; :: thesis: verum

end;

hence f is infs-preserving by WAYBEL_0:def 32; :: thesis: verum