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