let S, T be lower-bounded continuous Scott TopLattice; :: thesis:
let f be Function of S,T; :: thesis:
assume A1: 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:
A2: [#] T <> {} ;

now :: thesis:

let U1 be Subset of T; :: thesis:
assume A3: U1 is open ; :: thesis:
set U19 = U1;
A4: U1 is upper by A3, WAYBEL11:def 4;
reconsider fU = f " U1 as Subset of S ;
A5: Int fU c= fU by TOPS_1:16;
fU c= Int fU

proof

let xx be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: xx in fU ; :: thesis:
then reconsider x = xx as Element of S ;
A7: f . x in U1 by A6, FUNCT_1:def 7;
reconsider p = f . x as Element of T ;
consider u being Element of T such that
A8: u << p and
A9: u in U1 by A3, A7, Lm10;
consider w being Element of S such that
A10: w << x and
A11: u << f . w by A1, A8;
f .: (wayabove w) c= U1

proof

let h be object ; :: according to TARSKI:def 3 :: thesis:
assume h in f .: (wayabove w) ; :: thesis:
then consider z being object such that
A12: z in dom f and
A13: z in wayabove w and
A14: h = f . z by FUNCT_1:def 6;
reconsider z = z as Element of S by A12;
w << z by A13, WAYBEL_3:8;
then u << f . z by A1, A11;
then u <= f . z by WAYBEL_3:1;
hence h in U1 by A4, A9, A14; :: thesis:

end;

then A15: f " (f .: (wayabove w)) c= f " U1 by RELAT_1:143;
wayabove w c= f " (f .: (wayabove w)) by FUNCT_2:42;
then A16: wayabove w c= f " U1 by A15;
A17: Int fU = union { (wayabove g) where g is Element of S : wayabove g c= fU } by Lm14;
A18: x in wayabove w by A10;
wayabove w in { (wayabove g) where g is Element of S : wayabove g c= fU } by A16;
hence xx in Int fU by A17, A18, TARSKI:def 4; :: thesis:

end;

hence f " U1 is open by A5, XBOOLE_0:def 10; :: thesis:

end;

hence f is continuous by A2, TOPS_2:43; :: thesis: