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 <> {} ;
thus f is continuous :: thesis: verum

proof

now

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 U1' = U1;
A4: U1 is upper by A3, WAYBEL11:def 4;
reconsider fU = f " U1 as Subset of S ;
Int fU = fU

proof

thus Int fU c= fU by TOPS_1:44; :: according to XBOOLE_0:def 10 :: thesis: fU c= Int fU
thus fU c= Int fU :: thesis: verum

proof

let xx be set ; :: according to TARSKI:def 3 :: thesis: ( not xx in fU or xx in Int fU )
assume A5: xx in fU ; :: thesis: xx in Int fU
then reconsider x = xx as Element of S ;
A6: f . x in U1 by A5, FUNCT_1:def 13;
reconsider p = f . x as Element of T ;
consider u being Element of T such that
A7: ( u << p & u in U1 ) by A3, A6, Lm10;
consider w being Element of S such that
A8: ( w << x & u << f . w ) by A1, A7;
f .: (wayabove w) c= U1

proof

let h be set ; :: 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 set such that
A9: ( z in dom f & z in wayabove w & h = f . z ) by FUNCT_1:def 12;
reconsider z = z as Element of S by A9;
w << z by A9, WAYBEL_3:8;
then u << f . z by A1, A8;
then u <= f . z by WAYBEL_3:1;
hence h in U1 by A4, A7, A9, WAYBEL_0:def 20; :: thesis: verum

end;

then A10: f " (f .: (wayabove w)) c= f " U1 by RELAT_1:178;
wayabove w c= f " (f .: (wayabove w)) by FUNCT_2:50;
then A11: wayabove w c= f " U1 by A10, XBOOLE_1:1;
A12: Int fU = union { (wayabove g) where g is Element of S : wayabove g c= fU } by Lm14;
A13: x in wayabove w by A8;
wayabove w in { (wayabove g) where g is Element of S : wayabove g c= fU } by A11;
hence xx in Int fU by A12, A13, TARSKI:def 4; :: thesis: verum

end;

end;

hence f " U1 is open ; :: thesis: verum

end;

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

end;