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

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

let f be Function of S,T; :: thesis: ( f is continuous iff for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) implies f is continuous ) by Lm15; :: thesis: verum

( f is continuous iff for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

let f be Function of S,T; :: thesis: ( f is continuous iff for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

hereby :: thesis: ( ( for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) implies f is continuous )

thus
( ( for x being Element of Sfor y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) implies f is continuous )

assume
f is continuous
; :: thesis: for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

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

hence for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) by Th14; :: thesis: verum

end;for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

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

hence for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) by Th14; :: thesis: verum

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) implies f is continuous ) by Lm15; :: thesis: verum