theorem :: RFUNCT_4:20

for f being PartFunc of REAL,REAL
for I being Interval
for a being Real st ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I holds
f is_continuous_in a