theorem Th10: :: COUSIN2:11

for X being non empty real-membered bounded_below bounded_above set st upper_bound X = lower_bound X holds
ex r being Real st X = {r}