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 ( max+ r = r & max- r = 0 ) by XXREAL_0:def 10;
hence abs r = (max+ r) + (max- r) by A1, ABSVALUE:def 1; :: thesis: verum

end;

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

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

end;

end;

end;

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