let f be PartFunc of REAL,REAL; :: thesis: ( [#] REAL c= dom f & f | ([#] REAL) is continuous & ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) implies rng f is open )
set L = [#] REAL;
assume that
A1: [#] REAL c= dom f and
A2: f | ([#] REAL) is continuous and
A3: ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) ; :: thesis: rng f is open

now :: thesis: for r1 being Element of REAL st r1 in rng f holds
ex N being Neighbourhood of r1 st N c= rng f

let r1 be Element of REAL ; :: thesis: ( r1 in rng f implies ex N being Neighbourhood of r1 st N c= rng f )
assume r1 in rng f ; :: thesis: ex N being Neighbourhood of r1 st N c= rng f
then consider x0 being Element of REAL such that
A4: x0 in dom f and
A5: f . x0 = r1 by PARTFUN1:3;
A6: x0 in ([#] REAL) /\ (dom f) by A4, XBOOLE_0:def 4;
set N = the Neighbourhood of x0;
consider r being Real such that
A7: 0 < r and
A8: the Neighbourhood of x0 = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;
reconsider r = r as Element of REAL by XREAL_0:def 1;
0 < r / 2 by A7, XREAL_1:215;
then A9: x0 - (r / 2) < x0 - 0 by XREAL_1:15;
A10: r / 2 < r by A7, XREAL_1:216;
then A11: x0 - r < x0 - (r / 2) by XREAL_1:15;
A12: x0 + (r / 2) < x0 + r by A10, XREAL_1:8;
A13: the Neighbourhood of x0 c= dom f by A1;
set fp = f . (x0 + (r / 2));
set fm = f . (x0 - (r / 2));
A14: f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is continuous by A2, FCONT_1:16;
A15: x0 < x0 + (r / 2) by A7, XREAL_1:29, XREAL_1:215;
then A16: x0 - (r / 2) < x0 + (r / 2) by A9, XXREAL_0:2;
x0 - r < x0 by A7, XREAL_1:44;
then x0 - r < x0 + (r / 2) by A15, XXREAL_0:2;
then A17: x0 + (r / 2) in ].(x0 - r),(x0 + r).[ by A12;
then A18: x0 + (r / 2) in ([#] REAL) /\ (dom f) by A8, A13, XBOOLE_0:def 4;
x0 < x0 + r by A7, XREAL_1:29;
then x0 - (r / 2) < x0 + r by A9, XXREAL_0:2;
then A19: x0 - (r / 2) in ].(x0 - r),(x0 + r).[ by A11;
then A20: x0 - (r / 2) in ([#] REAL) /\ (dom f) by A8, A13, XBOOLE_0:def 4;
A21: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[ by A19, A17, XXREAL_2:def 12;

now :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng f

per cases ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) by A3;

suppose A22: f | ([#] REAL) is increasing ; :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng f

set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)));
f . x0 < f . (x0 + (r / 2)) by A15, A18, A6, A22, RFUNCT_2:20;
then A23: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50;
f . (x0 - (r / 2)) < f . x0 by A9, A20, A6, A22, RFUNCT_2:20;
then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50;
then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A23, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def 6;
take N1 = N1; :: thesis: N1 c= rng f
f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A16, A18, A20, A22, RFUNCT_2:20;
then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29;
then A24: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ;
thus N1 c= rng f :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng f )
A25: ( [.(x0 - (r / 2)),(x0 + (r / 2)).] c= dom f & ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ) by A1, XXREAL_1:25;
assume x in N1 ; :: thesis: x in rng f
then consider r2 being Real such that
A26: r2 = x and
A27: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and
A28: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A5;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7;
then A29: r2 < f . (x0 + (r / 2)) by A28, XXREAL_0:2;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13;
then f . (x0 - (r / 2)) < r2 by A27, XXREAL_0:2;
then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A29;
then consider s being Real such that
A30: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A31: x = f . s by A9, A15, A14, A24, A26, A25, FCONT_2:15, XXREAL_0:2;
s in the Neighbourhood of x0 by A8, A21, A30;
hence x in rng f by A13, A31, FUNCT_1:def 3; :: thesis: verum

end;

end;

suppose A32: f | ([#] REAL) is decreasing ; :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng f

set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))));
f . (x0 + (r / 2)) < f . x0 by A15, A18, A6, A32, RFUNCT_2:21;
then A33: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50;
f . x0 < f . (x0 - (r / 2)) by A9, A20, A6, A32, RFUNCT_2:21;
then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50;
then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A33, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def 6;
take N1 = N1; :: thesis: N1 c= rng f
f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A16, A18, A20, A32, RFUNCT_2:21;
then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29;
then A34: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ;
thus N1 c= rng f :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng f )
A35: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25;
assume x in N1 ; :: thesis: x in rng f
then consider r2 being Real such that
A36: r2 = x and
A37: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and
A38: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A5;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7;
then A39: r2 < f . (x0 - (r / 2)) by A38, XXREAL_0:2;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13;
then f . (x0 + (r / 2)) < r2 by A37, XXREAL_0:2;
then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A39;
then consider s being Real such that
A40: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A41: x = f . s by A1, A14, A16, A34, A36, A35, FCONT_2:15, XBOOLE_1:1;
s in the Neighbourhood of x0 by A8, A21, A40;
hence x in rng f by A13, A41, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

end;

hence ex N being Neighbourhood of r1 st N c= rng f ; :: thesis: verum

end;

hence rng f is open by RCOMP_1:20; :: thesis: verum