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 Th66; :: thesis: verum