theorem Th18: :: XXREAL_2:18

for x, y being ExtReal holds x is LowerBound of ].x,y.]