theorem Th9: :: SEQ_4:9

for r being Real holds
( lower_bound {r} = r & upper_bound {r} = r ) by XXREAL_2:11, XXREAL_2:13;