theorem :: RFUNCT_3:53

for a, b being Real
for F being PartFunc of REAL,REAL holds
( F is_convex_on [.a,b.] iff ( [.a,b.] c= dom F & ( for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds
((F . x1) - (F . x2)) / (x1 - x2) <= ((F . x2) - (F . x3)) / (x2 - x3) ) ) )