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
proof
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;
hence f . x <= f . y ; :: thesis: verum