theorem Th28: :: XXREAL_2:28

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