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