let F be PartFunc of REAL,REAL; :: thesis: for X being set st F is_convex_on X holds
max+ F is_convex_on X
let X be set ; :: thesis: ( F is_convex_on X implies max+ F is_convex_on X )
assume F is_convex_on X ; :: thesis: max+ F is_convex_on X
then max+ (F - 0) is_convex_on X by Th59;
hence max+ F is_convex_on X by Th48; :: thesis: verum