for x1, x2, l being Real st 0 <= l & l <= 1 holds
(EMF REAL) . ((l * x1) + ((1 - l) * x2)) >= min (((EMF REAL) . x1),((EMF REAL) . x2))

proof

let x1, x2 be Real; :: thesis: for l being Real st 0 <= l & l <= 1 holds
(EMF REAL) . ((l * x1) + ((1 - l) * x2)) >= min (((EMF REAL) . x1),((EMF REAL) . x2))
let l be Real; :: thesis: ( 0 <= l & l <= 1 implies (EMF REAL) . ((l * x1) + ((1 - l) * x2)) >= min (((EMF REAL) . x1),((EMF REAL) . x2)) )
set F = EMF REAL;
assume ( 0 <= l & l <= 1 ) ; :: thesis: (EMF REAL) . ((l * x1) + ((1 - l) * x2)) >= min (((EMF REAL) . x1),((EMF REAL) . x2))
A3: ( x1 in REAL & x2 in REAL ) by XREAL_0:def 1;
A1: ( (EMF REAL) . x1 = {} & (EMF REAL) . x2 = {} ) by FUNCT_3:def 3, A3;
(l * x1) + ((1 - l) * x2) in REAL by XREAL_0:def 1;
hence (EMF REAL) . ((l * x1) + ((1 - l) * x2)) >= min (((EMF REAL) . x1),((EMF REAL) . x2)) by A1, FUNCT_3:def 3; :: thesis: verum

end;

hence EMF REAL is f-convex ; :: thesis: verum