let S, T be complete Scott TopLattice; :: thesis:
let f be Function of S,T; :: thesis:
assume that
A1: S is algebraic and
A2: T is algebraic ; :: thesis:
A3: S is continuous by A1, WAYBEL_8:7;
A4: T is continuous by A2, WAYBEL_8:7;
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:
then A6: f is continuous by A3, A4, Th23;
let x be Element of S; :: thesis:
let k be Element of T; :: thesis:
assume A7: k in the carrier of (CompactSublatt T) ; :: thesis:

hereby :: thesis:

assume k <= f . x ; :: thesis:
then k << f . x by A7, WAYBEL_8:1;
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 (CompactSublatt S) and
A11: w <= w1 and
A12: w1 <= x by A1, A8, WAYBEL_8:7;
A13: k <= f . w by A9, WAYBEL_3:1;
take w1 = w1; :: thesis:
thus w1 in the carrier of (CompactSublatt S) by A10; :: thesis:
thus w1 <= x by A12; :: thesis:
f . w <= f . w1 by A6, A11, WAYBEL_1:def 2;
hence k <= f . w1 by A13, ORDERS_2:3; :: thesis:

end;

given j being Element of S such that j in the carrier of (CompactSublatt S) and
A14: j <= x and
A15: k <= f . j ; :: thesis:
f is continuous by A3, A4, A5, Lm15;
then f . j <= f . x by A14, WAYBEL_1:def 2;
hence k <= f . x by A15, ORDERS_2:3; :: thesis: