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 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 ) ) ) holds
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: ( S is algebraic & T is algebraic & ( 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 ) ) ) implies 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 ) ) )
assume A1: ( S is algebraic & T is algebraic ) ; :: thesis: ( ex x being Element of S ex k being Element of T st
( k in the carrier of (CompactSublatt T) & not ( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) or 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 ) ) )
assume A2: 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 ) ) ; :: 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 ) )
let x be Element of S; :: thesis: for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let y be Element of T; :: thesis: ( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )

hereby :: thesis: ( ex w being Element of S st
( w << x & y << f . w ) implies y << f . x )

assume y << f . x ; :: thesis: ex j being Element of S st
( j << x & y << f . j )
then consider w being Element of T such that
A3: ( w in the carrier of (CompactSublatt T) & y <= w & w <= f . x ) by A1, WAYBEL_8:7;
consider j being Element of S such that
A4: ( j in the carrier of (CompactSublatt S) & j <= x & w <= f . j ) by A2, A3;
take j = j; :: thesis: ( j << x & y << f . j )
thus j << x by A4, WAYBEL_8:1; :: thesis: y << f . j
thus y << f . j by A3, A4, WAYBEL_8:1; :: thesis: verum

end;

given w being Element of S such that A5: ( w << x & y << f . w ) ; :: thesis: y << f . x
consider h being Element of T such that
A6: ( h in the carrier of (CompactSublatt T) & y <= h & h <= f . w ) by A1, A5, WAYBEL_8:7;
consider j being Element of S such that
A7: ( j in the carrier of (CompactSublatt S) & j <= w & h <= f . j ) by A2, A6;
j << x by A5, A7, WAYBEL_3:2;
then j <= x by WAYBEL_3:1;
then h <= f . x by A2, A6, A7;
hence y << f . x by A6, WAYBEL_8:1; :: thesis: verum