let S be RealNormSpace; :: thesis: for f being PartFunc of the carrier of S,REAL
for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds
ex x1, x2 being Point of S st
( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) )
let f be PartFunc of the carrier of S,REAL; :: thesis: for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds
ex x1, x2 being Point of S st
( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) )
let Y be Subset of S; :: thesis: ( Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y implies ex x1, x2 being Point of S 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 is_continuous_on Y ; :: thesis: ex x1, x2 being Point of S 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 is_continuous_on Y

proof

thus Y c= dom (f | Y) by A5; :: according to NFCONT_1:def 8 :: thesis: for x0 being Point of S st x0 in Y holds
(f | Y) | Y is_continuous_in x0
let r be Point of S; :: thesis: ( r in Y implies (f | Y) | Y is_continuous_in r )
assume r in Y ; :: thesis: (f | Y) | Y is_continuous_in r
then f | Y is_continuous_in r by A4;
hence (f | Y) | Y is_continuous_in r by RELAT_1:72; :: thesis: verum

end;

then consider x1, x2 being Point of S 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, Th33;
take x1 ; :: thesis: ex x2 being Point of S 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 A5, A6; :: thesis: ( f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) )
( (f | Y) /. x1 = f /. x1 & (f | Y) /. x2 = f /. x2 ) by A6, PARTFUN2:15;
hence ( f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) by A7, RELAT_1:115; :: thesis: verum