let S, T be complete Scott TopLattice; :: thesis:
let f be Function of S,T; :: thesis:
assume A1: T is algebraic ; :: thesis:
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:
let x be Element of S; :: thesis:
let y be Element of T; :: thesis:

assume y << f . x ; :: thesis:
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:
thus j << x by A6, A7, WAYBEL_8:1; :: thesis:
thus y << f . j by A3, A4, A8, WAYBEL_8:1; :: thesis:

end;

given w being Element of S such that A9: w << x and
A10: y << f . w ; :: thesis:
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: