let X be non empty set ; :: thesis:
let f, g be Function of X,REAL; :: thesis:

now :: thesis:

let x be Element of X; :: thesis:
(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:

end;

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