for X being real-membered non empty set st X is bounded_below holds
inf X in REAL