theorem Th26: :: XXREAL_0:26
for a, b, c, d being ExtReal st a <= b & c <= d holds
max (a,c) <= max (b,d)