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

then ( x + y = -infty & x - y = -infty ) by A2, A3, XXREAL_3:14, XXREAL_3:def 2;
then A5: (x + y) - |.(x - y).| = -infty by Th67, XXREAL_3:14;
A6: min (x,y) = -infty by A4, XXREAL_0:44;
R_EAL 2 = 2 by MEASURE6:def 1;
hence min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) by A6, A5, 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 A8: y = -infty ; :: thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2)

then ( x + y = -infty & x - y = +infty ) by A1, A3, XXREAL_3:14, XXREAL_3:def 2;
then A9: (x + y) - |.(x - y).| = -infty by Th67, XXREAL_3:14;
A10: min (x,y) = -infty by A8, XXREAL_0:44;
R_EAL 2 = 2 by MEASURE6:def 1;
hence min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) by A10, A9, 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 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:5;
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;