theorem Th26: :: XXREAL_2:26

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