let r be real number ; :: thesis: 2 * (max+ r) = r + (abs r)
thus r + (abs r) = ((max+ r) - (max- r)) + (abs r) by Th1
.= ((max+ r) - (max- r)) + ((max+ r) + (max- r)) by Th2
.= 2 * (max+ r) ; :: thesis: verum