for X being ext-real-membered non empty set st ex y being UpperBound of X st y <> +infty holds
X is bounded_above