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 & y <> -infty ) and
A2: ( 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 A3: x = +infty ; :: thesis: max x,y = ((x + y) + |.(x - y).|) / (R_EAL 2)

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

then A8: max x,y = +infty by XXREAL_0:41;
A9: x + y = +infty by A1, A7, XXREAL_3:def 2;
x - y = -infty by A2, A7, XXREAL_3:13;
then A10: (x + y) + |.(x - y).| = +infty by A9, Th67, XXREAL_3:def 2;
( 0 < 2 & R_EAL 2 = 2 ) by MEASURE6:def 1;
then ( 0 < R_EAL 2 & R_EAL 2 < +infty ) by XXREAL_0:9;
hence max x,y = ((x + y) + |.(x - y).|) / (R_EAL 2) by A8, A10, 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 A1, XXREAL_0:14;
A11: x + y = a + b by SUPINF_2:1;
x - y = a - b by SUPINF_2:5;
then |.(x - y).| = abs (a - b) by Th49;
then A12: (x + y) + |.(x - y).| = (a + b) + (abs (a - b)) by A11, SUPINF_2:1;
( 0 < 2 & 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;