let S, T be non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr ; :: thesis: for f being Function of S,T st f is directed-sups-preserving holds
f is continuous
let f be Function of S,T; :: thesis: ( f is directed-sups-preserving implies f is continuous )
assume A1: f is directed-sups-preserving ; :: thesis: f is continuous
then A2: f is monotone ;
thus f is continuous :: thesis: verum

proof

let P1 be Subset of T; :: according to PRE_TOPC:def 12 :: thesis: ( not P1 is closed or f " P1 is closed )
reconsider P1' = P1 as Subset of T ;
assume P1 is closed ; :: thesis: f " P1 is closed
then A3: ( P1' is closed_under_directed_sups & P1' is lower ) by WAYBEL11:7;

now

let D be non empty directed Subset of S; :: thesis: ( D c= f " P1 implies sup D in f " P1 )
assume A4: D c= f " P1 ; :: thesis: sup D in f " P1
A5: f preserves_sup_of D by A1, WAYBEL_0:def 37;
ex_sup_of D,S by WAYBEL_0:75;
then A6: sup (f .: D) = f . (sup D) by A5, WAYBEL_0:def 31;
reconsider fD = f .: D as directed Subset of T by A1, YELLOW_2:17;
fD c= P1 by A4, BORSUK_1:5;
then sup fD in P1' by A3, WAYBEL11:def 2;
hence sup D in f " P1 by A6, FUNCT_2:46; :: thesis: verum

end;

then ( f " P1 is closed_under_directed_sups & f " P1 is lower ) by A2, A3, Th1, WAYBEL11:def 2;
hence f " P1 is closed by WAYBEL11:7; :: thesis: verum

end;