let S, T be complete Scott TopLattice; 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; ( 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 that
A1:
S is algebraic
and
A2:
T is algebraic
; ( 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) )
A3:
S is continuous
by A1, WAYBEL_8:7;
A4:
T is continuous
by A2, WAYBEL_8:7;
assume
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)
; 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 A3, A4, Th24; verum