theorem :: FCONT_2:18

for g, p being Real
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 )