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;
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 ) )
per cases ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) by A1, A2, A3, A4, Th17;
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 ) )
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;
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: verum
end;
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 ) )
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;
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: verum
end;
end;
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: verum