theorem Th4: :: RATFUNC1:4

for x, y, z being Integer holds max ((x + y),(x + z)) = x + (max (y,z))