for x, y being ExtReal st x < y holds
].x,y.] is right_end