let p, g be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing holds
f | [.p,g.] is decreasing
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing implies f | [.p,g.] is decreasing )
assume that
A1: f is one-to-one and
A4: [.p,g.] c= dom f and
A2: ( p <= g & f | [.p,g.] is continuous ) and
A3: ( not f | [.p,g.] is increasing & not f | [.p,g.] is decreasing ) ; :: thesis: contradiction

now

per cases ( p = g or p <> g ) ;

suppose p = g ; :: thesis: contradiction

then [.p,g.] = {p} by XXREAL_1:17;
hence contradiction by A3, RFUNCT_2:76; :: thesis: verum

end;

suppose A5: p <> g ; :: thesis: contradiction

A6: ( p in [.p,g.] & g in [.p,g.] ) by A2, XXREAL_1:1;
then A7: f . p <> f . g by A1, A4, A5, FUNCT_1:def 8;

now

per cases ( f . p < f . g or f . p > f . g ) by A7, XXREAL_0:1;

suppose A8: f . p < f . g ; :: thesis: contradiction

A9: for x1 being Real st p <= x1 & x1 <= g holds
( f . p <= f . x1 & f . x1 <= f . g )

proof

let x1 be Real; :: thesis: ( p <= x1 & x1 <= g implies ( f . p <= f . x1 & f . x1 <= f . g ) )
assume that
A10: ( p <= x1 & x1 <= g ) and
A11: ( not f . p <= f . x1 or not f . x1 <= f . g ) ; :: thesis: contradiction

now

per cases ( f . x1 < f . p or f . g < f . x1 ) by A11;

suppose A12: f . x1 < f . p ; :: thesis: contradiction

A13: x1 > p by A10, A12, XXREAL_0:1;
x1 in { r where r is Real : ( p <= r & r <= g ) } by A10;
then A14: x1 in [.p,g.] by RCOMP_1:def 1;
g in [.p,g.] by A2, XXREAL_1:1;
then A16: [.x1,g.] c= [.p,g.] by A14, XXREAL_2:def 12;
f . p in { r where r is Real : ( f . x1 <= r & r <= f . g ) } by A8, A12;
then f . p in [.(f . x1),(f . g).] by RCOMP_1:def 1;
then Q: f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def 3;
f | [.x1,g.] is continuous by A2, A16, FCONT_1:17;
then consider s being Real such that
A18: ( s in [.x1,g.] & f . s = f . p ) by A10, Th16, A16, Q, A4, XBOOLE_1:1;
A19: s in [.p,g.] by A16, A18;
s in { t where t is Real : ( x1 <= t & t <= g ) } by A18, RCOMP_1:def 1;
then ex r being Real st
( r = s & x1 <= r & r <= g ) ;
hence contradiction by A1, A4, A6, A13, A18, A19, FUNCT_1:def 8; :: thesis: verum

end;

suppose A20: f . g < f . x1 ; :: thesis: contradiction

x1 in { r where r is Real : ( p <= r & r <= g ) } by A10;
then A22: x1 in [.p,g.] by RCOMP_1:def 1;
p in [.p,g.] by A2, XXREAL_1:1;
then A24: [.p,x1.] c= [.p,g.] by A22, XXREAL_2:def 12;
f . g in { r where r is Real : ( f . p <= r & r <= f . x1 ) } by A8, A20;
then f . g in [.(f . p),(f . x1).] by RCOMP_1:def 1;
then Q: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def 3;
f | [.p,x1.] is continuous by A2, A24, FCONT_1:17;
then consider s being Real such that
A26: ( s in [.p,x1.] & f . s = f . g ) by A10, Th16, A24, Q, A4, XBOOLE_1:1;
s in [.p,g.] by A24, A26;
then A27: s = g by A1, A4, A6, A26, FUNCT_1:def 8;
s in { t where t is Real : ( p <= t & t <= x1 ) } by A26, RCOMP_1:def 1;
then ex r being Real st
( r = s & p <= r & r <= x1 ) ;
hence contradiction by A10, A20, A27, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

consider x1, x2 being Real such that
A28: ( x1 in [.p,g.] /\ (dom f) & x2 in [.p,g.] /\ (dom f) & x1 < x2 & f . x2 <= f . x1 ) by A3, RFUNCT_2:43;
A29: ( x1 in [.p,g.] & x2 in [.p,g.] & x1 in dom f & x2 in dom f ) by A28, XBOOLE_0:def 4;
then ( x1 in { t where t is Real : ( p <= t & t <= g ) } & x2 in { r where r is Real : ( p <= r & r <= g ) } ) by RCOMP_1:def 1;
then ( x1 in { t where t is Real : ( p <= t & t <= g ) } & ex r being Real st
( r = x2 & p <= r & r <= g ) ) ;
then A30: ( ex r being Real st
( r = x1 & p <= r & r <= g ) & p <= x2 & x2 <= g ) ;
then ( f . p <= f . x2 & f . x1 <= f . g ) by A9;
then f . x2 in { r where r is Real : ( f . p <= r & r <= f . x1 ) } by A28;
then f . x2 in [.(f . p),(f . x1).] by RCOMP_1:def 1;
then A31: f . x2 in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def 3;
[.p,x1.] c= [.p,g.] by A29, A6, XXREAL_2:def 12;
then T: [.p,x1.] c= dom f by A4, XBOOLE_1:1;
p in [.p,g.] by A2, XXREAL_1:1;
then A33: [.p,x1.] c= [.p,g.] by A29, XXREAL_2:def 12;
then f | [.p,x1.] is continuous by A2, FCONT_1:17;
then consider s being Real such that
A34: ( s in [.p,x1.] & f . s = f . x2 ) by A30, A31, Th16, T;
A35: s in [.p,g.] by A33, A34;
s in { t where t is Real : ( p <= t & t <= x1 ) } by A34, RCOMP_1:def 1;
then ex r being Real st
( r = s & p <= r & r <= x1 ) ;
hence contradiction by A1, A4, A28, A29, A34, A35, FUNCT_1:def 8; :: thesis: verum

end;

suppose A36: f . p > f . g ; :: thesis: contradiction

A37: for x1 being Real st p <= x1 & x1 <= g holds
( f . g <= f . x1 & f . x1 <= f . p )

proof

let x1 be Real; :: thesis: ( p <= x1 & x1 <= g implies ( f . g <= f . x1 & f . x1 <= f . p ) )
assume that
A38: ( p <= x1 & x1 <= g ) and
A39: ( not f . g <= f . x1 or not f . x1 <= f . p ) ; :: thesis: contradiction

now

per cases ( f . x1 < f . g or f . p < f . x1 ) by A39;

suppose A40: f . x1 < f . g ; :: thesis: contradiction

now

per cases ( g = x1 or g <> x1 ) ;

suppose g = x1 ; :: thesis: contradiction

hence contradiction by A40; :: thesis: verum

end;

suppose A41: g <> x1 ; :: thesis: contradiction

x1 in { r where r is Real : ( p <= r & r <= g ) } by A38;
then A42: x1 in [.p,g.] by RCOMP_1:def 1;
p in [.p,g.] by A2, XXREAL_1:1;
then A44: [.p,x1.] c= [.p,g.] by A42, XXREAL_2:def 12;
f . g in { r where r is Real : ( f . x1 <= r & r <= f . p ) } by A36, A40;
then f . g in [.(f . x1),(f . p).] by RCOMP_1:def 1;
then Q: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def 3;
f | [.p,x1.] is continuous by A2, A44, FCONT_1:17;
then consider s being Real such that
A46: ( s in [.p,x1.] & f . s = f . g ) by A38, Th16, A44, Q, A4, XBOOLE_1:1;
s in [.p,g.] by A44, A46;
then A47: s = g by A1, A4, A6, A46, FUNCT_1:def 8;
s in { t where t is Real : ( p <= t & t <= x1 ) } by A46, RCOMP_1:def 1;
then ex r being Real st
( r = s & p <= r & r <= x1 ) ;
hence contradiction by A38, A41, A47, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A48: f . p < f . x1 ; :: thesis: contradiction

now

per cases ( p = x1 or p <> x1 ) ;

suppose p = x1 ; :: thesis: contradiction

hence contradiction by A48; :: thesis: verum

end;

suppose A49: p <> x1 ; :: thesis: contradiction

x1 in { r where r is Real : ( p <= r & r <= g ) } by A38;
then A50: x1 in [.p,g.] by RCOMP_1:def 1;
g in [.p,g.] by A2, XXREAL_1:1;
then A52: [.x1,g.] c= [.p,g.] by A50, XXREAL_2:def 12;
then A53: f | [.x1,g.] is continuous by A2, FCONT_1:17;
f . p in { r where r is Real : ( f . g <= r & r <= f . x1 ) } by A36, A48;
then f . p in [.(f . g),(f . x1).] by RCOMP_1:def 1;
then f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def 3;
then consider s being Real such that
A54: ( s in [.x1,g.] & f . s = f . p ) by A38, A53, Th16, A52, A4, XBOOLE_1:1;
s in [.p,g.] by A52, A54;
then A55: s = p by A1, A4, A6, A54, FUNCT_1:def 8;
s in { t where t is Real : ( x1 <= t & t <= g ) } by A54, RCOMP_1:def 1;
then ex r being Real st
( r = s & x1 <= r & r <= g ) ;
hence contradiction by A38, A49, A55, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

consider x1, x2 being Real such that
A56: ( x1 in [.p,g.] /\ (dom f) & x2 in [.p,g.] /\ (dom f) & x1 < x2 & f . x1 <= f . x2 ) by A3, RFUNCT_2:44;
A57: ( x1 in [.p,g.] & x2 in [.p,g.] & x1 in dom f & x2 in dom f ) by A56, XBOOLE_0:def 4;
then ( x1 in { t where t is Real : ( p <= t & t <= g ) } & x2 in { r where r is Real : ( p <= r & r <= g ) } ) by RCOMP_1:def 1;
then A58: ( x1 in { t where t is Real : ( p <= t & t <= g ) } & ex r being Real st
( r = x2 & p <= r & r <= g ) ) ;
then ( ex r being Real st
( r = x1 & p <= r & r <= g ) & p <= x2 & x2 <= g ) ;
then ( f . g <= f . x1 & f . x2 <= f . p ) by A37;
then f . x1 in { r where r is Real : ( f . g <= r & r <= f . x2 ) } by A56;
then f . x1 in [.(f . g),(f . x2).] by RCOMP_1:def 1;
then A59: f . x1 in [.(f . x2),(f . g).] \/ [.(f . g),(f . x2).] by XBOOLE_0:def 3;
[.x2,g.] c= [.p,g.] by A57, A6, XXREAL_2:def 12;
then T: [.x2,g.] c= dom f by A4, XBOOLE_1:1;
g in [.p,g.] by A2, XXREAL_1:1;
then A61: [.x2,g.] c= [.p,g.] by A57, XXREAL_2:def 12;
then f | [.x2,g.] is continuous by A2, FCONT_1:17;
then consider s being Real such that
A62: ( s in [.x2,g.] & f . s = f . x1 ) by A58, A59, Th16, T;
A63: s in [.p,g.] by A61, A62;
s in { t where t is Real : ( x2 <= t & t <= g ) } by A62, RCOMP_1:def 1;
then ex r being Real st
( r = s & x2 <= r & r <= g ) ;
hence contradiction by A1, A4, A56, A57, A62, A63, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum