let S, T be up-complete Scott TopLattice; :: thesis: for f being Function of S,T st f is continuous holds

f is monotone

let f be Function of S,T; :: thesis: ( f is continuous implies f is monotone )

assume A1: f is continuous ; :: thesis: f is monotone

let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or f . x <= f . y )

A2: dom f = the carrier of S by FUNCT_2:def 1;

assume A3: x <= y ; :: thesis: f . x <= f . y

f . x <= f . y

f is monotone

let f be Function of S,T; :: thesis: ( f is continuous implies f is monotone )

assume A1: f is continuous ; :: thesis: f is monotone

let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or f . x <= f . y )

A2: dom f = the carrier of S by FUNCT_2:def 1;

assume A3: x <= y ; :: thesis: f . x <= f . y

f . x <= f . y

proof

hence
f . x <= f . y
; :: thesis: verum
set V = (downarrow (f . y)) ` ;

set U1 = f " ((downarrow (f . y)) `);

assume not f . x <= f . y ; :: thesis: contradiction

then not f . x in downarrow (f . y) by WAYBEL_0:17;

then A4: f . x in (downarrow (f . y)) ` by XBOOLE_0:def 5;

f . y <= f . y ;

then A5: f . y in downarrow (f . y) by WAYBEL_0:17;

downarrow (f . y) is closed by Lm3;

then f " ((downarrow (f . y)) `) is open by A1, TOPS_2:43;

then reconsider U1 = f " ((downarrow (f . y)) `) as upper Subset of S by WAYBEL11:def 4;

x in U1 by A2, A4, FUNCT_1:def 7;

then y in U1 by A3, WAYBEL_0:def 20;

then f . y in (downarrow (f . y)) ` by FUNCT_1:def 7;

hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;set U1 = f " ((downarrow (f . y)) `);

assume not f . x <= f . y ; :: thesis: contradiction

then not f . x in downarrow (f . y) by WAYBEL_0:17;

then A4: f . x in (downarrow (f . y)) ` by XBOOLE_0:def 5;

f . y <= f . y ;

then A5: f . y in downarrow (f . y) by WAYBEL_0:17;

downarrow (f . y) is closed by Lm3;

then f " ((downarrow (f . y)) `) is open by A1, TOPS_2:43;

then reconsider U1 = f " ((downarrow (f . y)) `) as upper Subset of S by WAYBEL11:def 4;

x in U1 by A2, A4, FUNCT_1:def 7;

then y in U1 by A3, WAYBEL_0:def 20;

then f . y in (downarrow (f . y)) ` by FUNCT_1:def 7;

hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum