let S, T be complete Scott TopLattice; :: thesis: for f being Function of S,T st 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: ( 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: 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) and
A4: y <= w and
A5: w <= f . x by A1, WAYBEL_8:7;
consider j being Element of S such that
A6: j in the carrier of (CompactSublatt S) and
A7: j <= x and
A8: w <= f . j by A2, A3, A5;
take j = j; :: thesis: ( j << x & y << f . j )
thus j << x by A6, A7, WAYBEL_8:1; :: thesis: y << f . j
thus y << f . j by A3, A4, A8, WAYBEL_8:1; :: thesis: verum

end;

given w being Element of S such that A9: w << x and
A10: y << f . w ; :: thesis: y << f . x
consider h being Element of T such that
A11: h in the carrier of (CompactSublatt T) and
A12: y <= h and
A13: h <= f . w by A1, A10, WAYBEL_8:7;
consider j being Element of S such that
A14: j in the carrier of (CompactSublatt S) and
A15: j <= w and
A16: h <= f . j by A2, A11, A13;
j << x by A9, A15, WAYBEL_3:2;
then j <= x by WAYBEL_3:1;
then h <= f . x by A2, A11, A14, A16;
hence y << f . x by A11, A12, WAYBEL_8:1; :: thesis: verum