theorem Th14: :: RCOMP_3:14

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