let x, y be ExtReal; :: thesis: ( x <> -infty & y <> -infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) implies max (x,y) = ((x + y) + |.(x - y).|) / 2 )
assume that
A1: x <> -infty and
A2: y <> -infty and
A3: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) ) ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2

per cases ( x = +infty or x <> +infty ) ;

suppose A4: x = +infty ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2

then ( x + y = +infty & x - y = +infty ) by A2, A3, XXREAL_3:13, XXREAL_3:def 2;
then A5: (x + y) + |.(x - y).| = +infty by XXREAL_3:def 2;
A6: max (x,y) = +infty by A4, XXREAL_0:41;
thus max (x,y) = ((x + y) + |.(x - y).|) / 2 by A6, A5, XXREAL_3:83; :: thesis: verum

end;

suppose x <> +infty ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2

then reconsider a = x as Element of REAL by A1, XXREAL_0:14;

per cases ( y = +infty or y <> +infty ) ;

suppose A7: y = +infty ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2

then ( x + y = +infty & x - y = -infty ) by A1, A3, XXREAL_3:13, XXREAL_3:def 2;
then A8: (x + y) + |.(x - y).| = +infty by XXREAL_3:def 2;
A9: max (x,y) = +infty by A7, XXREAL_0:41;
thus max (x,y) = ((x + y) + |.(x - y).|) / 2 by A9, A8, XXREAL_3:83; :: thesis: verum

end;

suppose y <> +infty ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2

then reconsider b = y as Element of REAL by A2, XXREAL_0:14;
x - y = a - b by SUPINF_2:3;
then ( x + y = a + b & |.(x - y).| = |.(a - b).| ) by SUPINF_2:1;
then A10: (x + y) + |.(x - y).| = (a + b) + |.(a - b).| by SUPINF_2:1;
((x + y) + |.(x - y).|) / 2 = ((a + b) + |.(a - b).|) / 2 by A10, Th2;
hence max (x,y) = ((x + y) + |.(x - y).|) / 2 by COMPLEX1:74; :: thesis: verum

end;

end;

end;

end;