let x, y be R_eal; :: thesis: ( x <> -infty & y <> -infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) implies max x,y = ((x + y) + |.(x - y).|) / (R_EAL 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).|) / (R_EAL 2)

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

suppose A4: x = +infty ; :: thesis: max x,y = ((x + y) + |.(x - y).|) / (R_EAL 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 Th67, XXREAL_3:def 2;
A6: max x,y = +infty by A4, XXREAL_0:41;
A7: R_EAL 2 = 2 by MEASURE6:def 1;
then R_EAL 2 < +infty by XXREAL_0:9;
hence max x,y = ((x + y) + |.(x - y).|) / (R_EAL 2) by A6, A5, A7, XXREAL_3:94; :: thesis: verum

end;

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

then reconsider a = x as Real by A1, XXREAL_0:14;

now

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

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

then ( x + y = +infty & x - y = -infty ) by A1, A3, XXREAL_3:13, XXREAL_3:def 2;
then A9: (x + y) + |.(x - y).| = +infty by Th67, XXREAL_3:def 2;
A10: max x,y = +infty by A8, XXREAL_0:41;
A11: R_EAL 2 = 2 by MEASURE6:def 1;
then R_EAL 2 < +infty by XXREAL_0:9;
hence max x,y = ((x + y) + |.(x - y).|) / (R_EAL 2) by A10, A9, A11, XXREAL_3:94; :: thesis: verum

end;

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

then reconsider b = y as Real by A2, XXREAL_0:14;
x - y = a - b by SUPINF_2:5;
then ( x + y = a + b & |.(x - y).| = abs (a - b) ) by Th49, SUPINF_2:1;
then A12: (x + y) + |.(x - y).| = (a + b) + (abs (a - b)) by SUPINF_2:1;
R_EAL 2 = 2 by MEASURE6:def 1;
then ((x + y) + |.(x - y).|) / (R_EAL 2) = ((a + b) + (abs (a - b))) / 2 by A12, EXTREAL1:32;
hence max x,y = ((x + y) + |.(x - y).|) / (R_EAL 2) by COMPLEX1:160; :: thesis: verum

end;

end;

end;

hence max x,y = ((x + y) + |.(x - y).|) / (R_EAL 2) ; :: thesis: verum

end;

end;