let f be PartFunc of REAL,REAL; :: thesis: for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is continuous holds

ex x1, x2 being Real st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

let Y be Subset of REAL; :: thesis: ( Y <> {} & Y c= dom f & Y is compact & f | Y is continuous implies ex x1, x2 being Real st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) )

assume that

A1: Y <> {} and

A2: Y c= dom f and

A3: Y is compact and

A4: f | Y is continuous ; :: thesis: ex x1, x2 being Real st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

A5: dom (f | Y) = (dom f) /\ Y by RELAT_1:61

.= Y by A2, XBOOLE_1:28 ;

(f | Y) | Y is continuous by A4;

then consider x1, x2 being Real such that

A6: ( x1 in dom (f | Y) & x2 in dom (f | Y) ) and

A7: ( (f | Y) . x1 = upper_bound (rng (f | Y)) & (f | Y) . x2 = lower_bound (rng (f | Y)) ) by A1, A3, A5, Th30;

take x1 ; :: thesis: ex x2 being Real st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

take x2 ; :: thesis: ( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

thus ( x1 in Y & x2 in Y ) by A6; :: thesis: ( f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

( f . x1 = upper_bound (rng (f | Y)) & f . x2 = lower_bound (rng (f | Y)) ) by A6, A7, FUNCT_1:47;

hence ( f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) by RELAT_1:115; :: thesis: verum

ex x1, x2 being Real st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

let Y be Subset of REAL; :: thesis: ( Y <> {} & Y c= dom f & Y is compact & f | Y is continuous implies ex x1, x2 being Real st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) )

assume that

A1: Y <> {} and

A2: Y c= dom f and

A3: Y is compact and

A4: f | Y is continuous ; :: thesis: ex x1, x2 being Real st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

A5: dom (f | Y) = (dom f) /\ Y by RELAT_1:61

.= Y by A2, XBOOLE_1:28 ;

(f | Y) | Y is continuous by A4;

then consider x1, x2 being Real such that

A6: ( x1 in dom (f | Y) & x2 in dom (f | Y) ) and

A7: ( (f | Y) . x1 = upper_bound (rng (f | Y)) & (f | Y) . x2 = lower_bound (rng (f | Y)) ) by A1, A3, A5, Th30;

take x1 ; :: thesis: ex x2 being Real st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

take x2 ; :: thesis: ( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

thus ( x1 in Y & x2 in Y ) by A6; :: thesis: ( f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

( f . x1 = upper_bound (rng (f | Y)) & f . x2 = lower_bound (rng (f | Y)) ) by A6, A7, FUNCT_1:47;

hence ( f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) by RELAT_1:115; :: thesis: verum