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