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 uniformly_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 uniformly_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 uniformly_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) )
ex x1, x2 being real number st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) by A1, A2, A3, A4, Th9, FCONT_1:32;
hence ex x1, x2 being Real st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) ; :: thesis: verum