let S, T be lower-bounded continuous Scott TopLattice; :: thesis: for f being Function of S,T st ( 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 ) ) ) holds
f is continuous
let f be Function of S,T; :: 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 ) ) ) implies f is continuous )
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: f is continuous
A2: [#] T <> {} ;

now :: thesis: for U1 being Subset of T st U1 is open holds
f " U1 is open

let U1 be Subset of T; :: thesis: ( U1 is open implies f " U1 is open )
assume A3: U1 is open ; :: thesis: f " U1 is open
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: ( not xx in fU or xx in Int fU )
assume A6: xx in fU ; :: thesis: xx in Int fU
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: ( not h in f .: (wayabove w) or h in U1 )
assume h in f .: (wayabove w) ; :: thesis: h in U1
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: verum

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: verum

end;

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

end;

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