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 (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & 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 (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
assume A1: ( S is algebraic & 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 (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
then A2: ( S is continuous & T is continuous ) by WAYBEL_8:7;
assume A3: 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 (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
then f is continuous by A2, Th23;
then A4: f is monotone ;
let x be Element of S; :: thesis: for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
let k be Element of T; :: thesis: ( k in the carrier of (CompactSublatt T) implies ( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
assume A5: k in the carrier of (CompactSublatt T) ; :: thesis: ( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

hereby :: thesis: ( ex j being Element of S st
( j in the carrier of (CompactSublatt S) & 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 (CompactSublatt S) & w1 <= x & k <= f . w1 )
then k << f . x by A5, WAYBEL_8:1;
then consider w being Element of S such that
A6: ( w << x & k << f . w ) by A3;
consider w1 being Element of S such that
A7: ( w1 in the carrier of (CompactSublatt S) & w <= w1 & w1 <= x ) by A1, A6, WAYBEL_8:7;
A8: ( w <= x & k <= f . w ) by A6, WAYBEL_3:1;
take w1 = w1; :: thesis: ( w1 in the carrier of (CompactSublatt S) & w1 <= x & k <= f . w1 )
thus w1 in the carrier of (CompactSublatt S) by A7; :: thesis: ( w1 <= x & k <= f . w1 )
thus w1 <= x by A7; :: thesis: k <= f . w1
f . w <= f . w1 by A4, A7, WAYBEL_1:def 2;
hence k <= f . w1 by A8, ORDERS_2:26; :: thesis: verum

end;

given j being Element of S such that A9: ( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ; :: thesis: k <= f . x
f is continuous by A2, A3, Lm15;
then f is monotone ;
then f . j <= f . x by A9, WAYBEL_1:def 2;
hence k <= f . x by A9, ORDERS_2:26; :: thesis: verum