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