let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for x being Element of X holds 0 <= (max- f) . x
let f be PartFunc of X,REAL; :: thesis: for x being Element of X holds 0 <= (max- f) . x
let x be Element of X; :: thesis: 0 <= (max- f) . x
0. <= (max- (R_EAL f)) . x by MESFUNC2:13;
hence 0 <= (max- f) . x by Th30; :: thesis: verum