theorem Th36: :: XXREAL_2:36

for x being ExtReal holds x is LowerBound of {}