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

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;

hence f " P1 is closed by WAYBEL11:7; :: thesis: verum

end;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

then
( f " P1 is directly_closed & f " P1 is lower )
by A1, A2, Th1;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;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

hence f " P1 is closed by WAYBEL11:7; :: thesis: verum