theorem Th27: :: XXREAL_2:27

for x, y being ExtReal st x < y holds
inf ].x,y.] = x