theorem Th19: :: XXREAL_2:19

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