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