let g, p be Real; :: thesis: for f being PartFunc of REAL,REAL st f is one-to-one & p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous & not ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) holds

( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p )

let f be PartFunc of REAL,REAL; :: thesis: ( f is one-to-one & p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous & not ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) implies ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )

assume that

A1: f is one-to-one and

A2: p <= g and

A3: [.p,g.] c= dom f and

A4: f | [.p,g.] is continuous ; :: thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )

A5: p in [.p,g.] by A2, XXREAL_1:1;

then A6: f . p in f .: [.p,g.] by A3, FUNCT_1:def 6;

A7: g in [.p,g.] by A2, XXREAL_1:1;

then A8: f . g in f .: [.p,g.] by A3, FUNCT_1:def 6;

A9: g in [.p,g.] /\ (dom f) by A3, A7, XBOOLE_0:def 4;

A10: p in [.p,g.] /\ (dom f) by A3, A5, XBOOLE_0:def 4;

[.p,g.] <> {} by A2, XXREAL_1:1;

then consider x1, x2 being Real such that

A11: x1 in [.p,g.] and

A12: x2 in [.p,g.] and

A13: f . x1 = upper_bound (f .: [.p,g.]) and

A14: f . x2 = lower_bound (f .: [.p,g.]) by A3, A4, FCONT_1:31, RCOMP_1:6;

A15: x2 in [.p,g.] /\ (dom f) by A3, A12, XBOOLE_0:def 4;

x2 in { t where t is Real : ( p <= t & t <= g ) } by A12, RCOMP_1:def 1;

then A16: ex r being Real st

( r = x2 & p <= r & r <= g ) ;

x1 in { r where r is Real : ( p <= r & r <= g ) } by A11, RCOMP_1:def 1;

then A17: ex r being Real st

( r = x1 & p <= r & r <= g ) ;

[.p,g.] is compact by RCOMP_1:6;

then A18: f .: [.p,g.] is real-bounded by A3, A4, FCONT_1:29, RCOMP_1:10;

A19: x1 in [.p,g.] /\ (dom f) by A3, A11, XBOOLE_0:def 4;

( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p )

let f be PartFunc of REAL,REAL; :: thesis: ( f is one-to-one & p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous & not ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) implies ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )

assume that

A1: f is one-to-one and

A2: p <= g and

A3: [.p,g.] c= dom f and

A4: f | [.p,g.] is continuous ; :: thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )

A5: p in [.p,g.] by A2, XXREAL_1:1;

then A6: f . p in f .: [.p,g.] by A3, FUNCT_1:def 6;

A7: g in [.p,g.] by A2, XXREAL_1:1;

then A8: f . g in f .: [.p,g.] by A3, FUNCT_1:def 6;

A9: g in [.p,g.] /\ (dom f) by A3, A7, XBOOLE_0:def 4;

A10: p in [.p,g.] /\ (dom f) by A3, A5, XBOOLE_0:def 4;

[.p,g.] <> {} by A2, XXREAL_1:1;

then consider x1, x2 being Real such that

A11: x1 in [.p,g.] and

A12: x2 in [.p,g.] and

A13: f . x1 = upper_bound (f .: [.p,g.]) and

A14: f . x2 = lower_bound (f .: [.p,g.]) by A3, A4, FCONT_1:31, RCOMP_1:6;

A15: x2 in [.p,g.] /\ (dom f) by A3, A12, XBOOLE_0:def 4;

x2 in { t where t is Real : ( p <= t & t <= g ) } by A12, RCOMP_1:def 1;

then A16: ex r being Real st

( r = x2 & p <= r & r <= g ) ;

x1 in { r where r is Real : ( p <= r & r <= g ) } by A11, RCOMP_1:def 1;

then A17: ex r being Real st

( r = x1 & p <= r & r <= g ) ;

[.p,g.] is compact by RCOMP_1:6;

then A18: f .: [.p,g.] is real-bounded by A3, A4, FCONT_1:29, RCOMP_1:10;

A19: x1 in [.p,g.] /\ (dom f) by A3, A11, XBOOLE_0:def 4;

now :: thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )end;

hence
( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )
; :: thesis: verumper cases
( f | [.p,g.] is increasing or f | [.p,g.] is decreasing )
by A1, A2, A3, A4, Th17;

end;

suppose A20:
f | [.p,g.] is increasing
; :: thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )

end;

A21: now :: thesis: not x1 <> g

assume
x1 <> g
; :: thesis: contradiction

then x1 < g by A17, XXREAL_0:1;

then f . x1 < f . g by A9, A19, A20, RFUNCT_2:20;

hence contradiction by A8, A18, A13, SEQ_4:def 1; :: thesis: verum

end;then x1 < g by A17, XXREAL_0:1;

then f . x1 < f . g by A9, A19, A20, RFUNCT_2:20;

hence contradiction by A8, A18, A13, SEQ_4:def 1; :: thesis: verum

now :: thesis: not x2 <> p

hence
( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )
by A13, A14, A21; :: thesis: verumassume
x2 <> p
; :: thesis: contradiction

then p < x2 by A16, XXREAL_0:1;

then f . p < f . x2 by A10, A15, A20, RFUNCT_2:20;

hence contradiction by A6, A18, A14, SEQ_4:def 2; :: thesis: verum

end;then p < x2 by A16, XXREAL_0:1;

then f . p < f . x2 by A10, A15, A20, RFUNCT_2:20;

hence contradiction by A6, A18, A14, SEQ_4:def 2; :: thesis: verum

suppose A22:
f | [.p,g.] is decreasing
; :: thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )

end;

A23: now :: thesis: not x2 <> g

assume
x2 <> g
; :: thesis: contradiction

then x2 < g by A16, XXREAL_0:1;

then f . g < f . x2 by A9, A15, A22, RFUNCT_2:21;

hence contradiction by A8, A18, A14, SEQ_4:def 2; :: thesis: verum

end;then x2 < g by A16, XXREAL_0:1;

then f . g < f . x2 by A9, A15, A22, RFUNCT_2:21;

hence contradiction by A8, A18, A14, SEQ_4:def 2; :: thesis: verum

now :: thesis: not x1 <> p

hence
( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) )
by A13, A14, A23; :: thesis: verumassume
x1 <> p
; :: thesis: contradiction

then p < x1 by A17, XXREAL_0:1;

then f . x1 < f . p by A10, A19, A22, RFUNCT_2:21;

hence contradiction by A6, A18, A13, SEQ_4:def 1; :: thesis: verum

end;then p < x1 by A17, XXREAL_0:1;

then f . x1 < f . p by A10, A19, A22, RFUNCT_2:21;

hence contradiction by A6, A18, A13, SEQ_4:def 1; :: thesis: verum