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