let S, T be complete Scott TopLattice; :: thesis: for f being Function of S,T st S is algebraic & T is algebraic holds
( f is continuous iff for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T )
let f be Function of S,T; :: thesis: ( S is algebraic & T is algebraic implies ( f is continuous iff for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T ) )
assume A1: ( S is algebraic & T is algebraic ) ; :: thesis: ( f is continuous iff for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T )
then A2: ( S is continuous & T is continuous ) by WAYBEL_8:7;

hereby :: thesis: ( ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T ) implies f is continuous )

assume f is continuous ; :: thesis: for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T
then for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T by A2, Th24;
hence for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T by A1, Lm19; :: thesis: verum

end;

assume for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T ; :: thesis: f is continuous
then for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T by Th26;
hence f is continuous by A2, Th24; :: thesis: verum