for X being ext-real-membered non empty set st ex y being LowerBound of X st y <> -infty holds
X is bounded_below