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
thus f is continuous :: thesis: verum

proof

let P1 be Subset of T; :: according to PRE_TOPC:def 6 :: thesis: ( not P1 is closed or f " P1 is closed )
reconsider P19 = P1 as Subset of T ;
assume P1 is closed ; :: thesis: f " P1 is closed
then A2: ( P19 is directly_closed & P19 is lower ) by WAYBEL11:7;

now :: thesis: for D being non empty directed Subset of S st D c= f " P1 holds
sup D in f " P1

let D be non empty directed Subset of S; :: thesis: ( D c= f " P1 implies sup D in f " P1 )
assume A3: D c= f " P1 ; :: thesis: sup D in f " P1
A4: f preserves_sup_of D by A1;
ex_sup_of D,S by WAYBEL_0:75;
then A5: sup (f .: D) = f . (sup D) by A4;
reconsider fD = f .: D as directed Subset of T by A1, YELLOW_2:15;
fD c= P1 by A3, EQREL_1:46;
then sup fD in P19 by A2;
hence sup D in f " P1 by A5, FUNCT_2:38; :: thesis: verum

end;

then ( f " P1 is directly_closed & f " P1 is lower ) by A1, A2, Th1;
hence f " P1 is closed by WAYBEL11:7; :: thesis: verum

end;