theorem Th15: :: XXREAL_2:15

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