theorem Th25: :: XXREAL_2:25

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