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

now

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

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

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

end;

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

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

end;

end;

end;

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