theorem Th25: :: XXREAL_0:25

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