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