theorem Th16: :: TOPREAL6:17

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