let S, T be complete Scott TopLattice; :: thesis: for f being Function of S,T st S is algebraic & T is algebraic & ( 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 ) ) ) holds
for x being Element of S
for k being Element of T st k in the carrier of () holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of () & j <= x & k <= f . j ) )

let f be Function of S,T; :: thesis: ( S is algebraic & T is algebraic & ( 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 for x being Element of S
for k being Element of T st k in the carrier of () holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of () & j <= x & k <= f . j ) ) )

assume that
A1: S is algebraic and
A2: T is algebraic ; :: thesis: ( ex x being Element of S ex y being Element of T st
( ( y << f . x implies ex w being Element of S st
( w << x & y << f . w ) ) implies ( ex w being Element of S st
( w << x & y << f . w ) & not y << f . x ) ) or for x being Element of S
for k being Element of T st k in the carrier of () holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of () & j <= x & k <= f . j ) ) )

A3: S is continuous by ;
A4: T is continuous by ;
assume A5: 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 ) ) ; :: thesis: for x being Element of S
for k being Element of T st k in the carrier of () holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of () & j <= x & k <= f . j ) )

then A6: f is continuous by A3, A4, Th23;
let x be Element of S; :: thesis: for k being Element of T st k in the carrier of () holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of () & j <= x & k <= f . j ) )

let k be Element of T; :: thesis: ( k in the carrier of () implies ( k <= f . x iff ex j being Element of S st
( j in the carrier of () & j <= x & k <= f . j ) ) )

assume A7: k in the carrier of () ; :: thesis: ( k <= f . x iff ex j being Element of S st
( j in the carrier of () & j <= x & k <= f . j ) )

hereby :: thesis: ( ex j being Element of S st
( j in the carrier of () & j <= x & k <= f . j ) implies k <= f . x )
assume k <= f . x ; :: thesis: ex w1 being Element of S st
( w1 in the carrier of () & w1 <= x & k <= f . w1 )

then k << f . x by ;
then consider w being Element of S such that
A8: w << x and
A9: k << f . w by A5;
consider w1 being Element of S such that
A10: w1 in the carrier of () and
A11: w <= w1 and
A12: w1 <= x by ;
A13: k <= f . w by ;
take w1 = w1; :: thesis: ( w1 in the carrier of () & w1 <= x & k <= f . w1 )
thus w1 in the carrier of () by A10; :: thesis: ( w1 <= x & k <= f . w1 )
thus w1 <= x by A12; :: thesis: k <= f . w1
f . w <= f . w1 by ;
hence k <= f . w1 by ; :: thesis: verum
end;
given j being Element of S such that j in the carrier of () and
A14: j <= x and
A15: k <= f . j ; :: thesis: k <= f . x
f is continuous by A3, A4, A5, Lm15;
then f . j <= f . x by ;
hence k <= f . x by ; :: thesis: verum