theorem Th17: :: XXREAL_0:17
for a, b being ExtReal holds min (a,b) <= a