for S being RealNormSpace
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) )