theorem Th35: :: XXREAL_2:35

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