let X be non empty set ; :: thesis: for f being Function of X,REAL holds
( f is with_min iff - f is with_max )
let f be Function of X,REAL ; :: thesis: ( f is with_min iff - f is with_max )
- (- f) = f ;
hence ( f is with_min iff - f is with_max ) by Lm7, Lm8; :: thesis: verum