theorem :: RFUNCT_3:54
for F being PartFunc of REAL,REAL
for X, Y being set st F is_convex_on X & Y c= X holds
F is_convex_on Y