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

now :: thesis: ( ( 0 <= r & r = (max+ r) - (max- r) ) or ( r < 0 & r = (max+ r) - (max- r) ) )

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

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

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 r < 0 ; :: thesis: r = (max+ r) - (max- r)

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

end;

end;

end;

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