theorem Th22: :: RCOMP_3:22

for X being Subset of REAL st X is bounded_above & not upper_bound X in X holds
X c= left_open_halfline (upper_bound X)