theorem Th17: :: XXREAL_2:17

for x, y being ExtReal holds x is LowerBound of [.x,y.]