theorem Th21: :: RCOMP_1:21

for X being Subset of REAL st X is open & X is bounded_above holds
not upper_bound X in X