theorem :: RFUNCT_3:62
for r being Real holds max+ ((id ([#] REAL)) - r) is_convex_on REAL by Th59, Th61;