theorem Th37: :: COUSIN2:41

for I being non empty closed_interval Subset of REAL
for f being bounded Function of I,REAL holds
( |.((upper_bound (rng f)) - (lower_bound (rng f))).| = 0 iff f is constant )