:: deftheorem defines max- RFUNCT_3:def 2 :
for r being Real holds max- r = max ((- r),0);