theorem Th5: :: RFUNCT_3:5

for r, s being Real holds max+ (r + s) <= (max+ r) + (max+ s)