theorem Th12: :: RCOMP_1:12

for X being Subset of REAL st X <> {} & X is closed & X is bounded_above holds
upper_bound X in X