theorem Th16: :: RCOMP_3:16

for X being real-bounded Subset of REAL st not upper_bound X in X holds
X c= [.(lower_bound X),(upper_bound X).[