theorem :: JORDAN5A:19

for a, b being Real st a <= b holds
( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b )