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

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

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

then A4: min x,y = -infty by XXREAL_0:44;
A5: x + y = -infty by A1, A3, XXREAL_3:def 2;
x - y = -infty by A2, A3, XXREAL_3:14;
then A6: (x + y) - |.(x - y).| = -infty by A5, Th67, XXREAL_3:14;
( 0 < 2 & R_EAL 2 = 2 ) by MEASURE6:def 1;
then ( 0 < R_EAL 2 & R_EAL 2 < +infty ) by XXREAL_0:9;
hence min x,y = ((x + y) - |.(x - y).|) / (R_EAL 2) by A4, A6, XXREAL_3:97; :: thesis: verum

end;

suppose x <> -infty ; :: thesis: min 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: min x,y = ((x + y) - |.(x - y).|) / (R_EAL 2)

then A8: min x,y = -infty by XXREAL_0:44;
A9: x + y = -infty by A1, A7, XXREAL_3:def 2;
x - y = +infty by A2, A7, XXREAL_3:14;
then A10: (x + y) - |.(x - y).| = -infty by A9, Th67, XXREAL_3:14;
( 0 < 2 & R_EAL 2 = 2 ) by MEASURE6:def 1;
then ( 0 < R_EAL 2 & R_EAL 2 < +infty ) by XXREAL_0:9;
hence min x,y = ((x + y) - |.(x - y).|) / (R_EAL 2) by A8, A10, XXREAL_3:97; :: thesis: verum

end;

suppose y <> -infty ; :: thesis: min 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:5;
( 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 min x,y = ((x + y) - |.(x - y).|) / (R_EAL 2) by COMPLEX1:159; :: thesis: verum

end;

end;

end;

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

end;

end;