let r be real number ; :: thesis: r = (max+ r) - (max- r)

now

per cases ( 0 <= r or r < 0 ) ;

case A1: 0 <= r ; :: thesis: r = (max+ r) - (max- r)

then - r <= - 0 ;
then max- r = 0 by XXREAL_0:def 10;
hence r = (max+ r) - (max- r) by A1, XXREAL_0:def 10; :: thesis: verum

end;

case A2: r < 0 ; :: thesis: r = (max+ r) - (max- r)

then A3: max+ r = 0 by XXREAL_0:def 10;
0 < - r by A2, XREAL_1:60;
then max- r = - r by XXREAL_0:def 10;
hence r = (max+ r) - (max- r) by A3; :: thesis: verum

end;

end;

end;

hence r = (max+ r) - (max- r) ; :: thesis: verum