theorem Th20: :: RCOMP_3:20

for X being Subset of REAL st X is bounded_above holds
X c= left_closed_halfline (upper_bound X)