theorem Th20: :: XXREAL_2:20

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