theorem Th17: :: XXREAL_0:17

for a, b being ExtReal holds min (a,b) <= a