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

( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) ) )

assume ( dom f <> {} & dom f is compact & f | (dom f) is continuous ) ; :: thesis: ex x1, x2 being Real st

( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) )

then A1: ( rng f <> {} & rng f is compact ) by Th28, RELAT_1:42;

then consider x being Element of REAL such that

A2: ( x in dom f & upper_bound (rng f) = f . x ) by PARTFUN1:3, RCOMP_1:14;

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

( x in dom f & x2 in dom f & f . x = upper_bound (rng f) & f . x2 = lower_bound (rng f) )

consider y being Element of REAL such that

A3: ( y in dom f & lower_bound (rng f) = f . y ) by A1, PARTFUN1:3, RCOMP_1:14;

take y ; :: thesis: ( x in dom f & y in dom f & f . x = upper_bound (rng f) & f . y = lower_bound (rng f) )

thus ( x in dom f & y in dom f & f . x = upper_bound (rng f) & f . y = lower_bound (rng f) ) by A2, A3; :: thesis: verum

( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) ) )

assume ( dom f <> {} & dom f is compact & f | (dom f) is continuous ) ; :: thesis: ex x1, x2 being Real st

( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) )

then A1: ( rng f <> {} & rng f is compact ) by Th28, RELAT_1:42;

then consider x being Element of REAL such that

A2: ( x in dom f & upper_bound (rng f) = f . x ) by PARTFUN1:3, RCOMP_1:14;

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

( x in dom f & x2 in dom f & f . x = upper_bound (rng f) & f . x2 = lower_bound (rng f) )

consider y being Element of REAL such that

A3: ( y in dom f & lower_bound (rng f) = f . y ) by A1, PARTFUN1:3, RCOMP_1:14;

take y ; :: thesis: ( x in dom f & y in dom f & f . x = upper_bound (rng f) & f . y = lower_bound (rng f) )

thus ( x in dom f & y in dom f & f . x = upper_bound (rng f) & f . y = lower_bound (rng f) ) by A2, A3; :: thesis: verum