let X be non empty set ; :: thesis: for f, g being Function of X,REAL holds min (f,g) <= f
let f, g be Function of X,REAL; :: thesis: min (f,g) <= f

now :: thesis: for x being Element of X holds
( (min (f,g)) . x <= f . x & (min (f,g)) . x <= g . x )

let x be Element of X; :: thesis: ( (min (f,g)) . x <= f . x & (min (f,g)) . x <= g . x )
(min (f,g)) . x = min ((f . x),(g . x)) by DEFM1;
hence ( (min (f,g)) . x <= f . x & (min (f,g)) . x <= g . x ) by XXREAL_0:17; :: thesis: verum

end;

hence min (f,g) <= f ; :: thesis: verum