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