theorem Th1: :: RFUNCT_3:1

for r being Real holds r = (max+ r) - (max- r)