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:

now :: thesis:

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

now :: thesis:

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

now :: thesis:

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

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) 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:

end;

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

end;

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

now :: thesis:

let X be Subset of S; :: thesis:

now :: thesis:

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

now :: thesis:

per cases ;

suppose f .: X = {} ; :: thesis:

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

end;

suppose f .: X <> {} ; :: thesis:

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:

end;

end;

end;

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

end;

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

end;

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