theorem :: XXREAL_2:42

for X being ext-real-membered set holds -infty is LowerBound of X