let S, T be complete continuous Scott TopLattice; :: thesis: for f being Function of S,T holds

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

let f be Function of S,T; :: thesis: ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )

thus ( f is continuous implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) by Th12; :: thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies f is continuous )

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

then f is directed-sups-preserving by Lm16;

hence f is continuous ; :: thesis: verum

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

let f be Function of S,T; :: thesis: ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )

thus ( f is continuous implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) by Th12; :: thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies f is continuous )

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

then f is directed-sups-preserving by Lm16;

hence f is continuous ; :: thesis: verum