for F being PartFunc of REAL,REAL
for X being set
for r being Real holds
( F is_convex_on X iff F - r is_convex_on X )