for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL st dom f <> {} & dom f is compact & f is_continuous_on dom f holds
ex x1, x2 being Point of CNS st
( x1 in dom f & x2 in dom f & f /. x1 = upper_bound (rng f) & f /. x2 = lower_bound (rng f) )