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 <> {} ;

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

hence
f is continuous
by A2, TOPS_2:43; :: thesis: verumf " 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

end;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

hence
f " U1 is open
by A5, XBOOLE_0:def 10; :: thesis: verum
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

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;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

then A15:
f " (f .: (wayabove w)) c= f " U1
by RELAT_1:143;
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;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

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