theorem :: COMPLEX1:74

for a, b being Real holds max (a,b) = ((a + b) + |.(a - b).|) / 2