let X be non empty set ; :: thesis: for f being Function of X,REAL st f is with_max holds
- f is with_min
let f be Function of X,REAL; :: thesis: ( f is with_max implies - f is with_min )
assume that
A1: f .: X is bounded_above and
A2: upper_bound (f .: X) in f .: X ; :: according to MEASURE6:def 4,MEASURE6:def 12 :: thesis: - f is with_min
A3: -- (f .: X) = (- f) .: X by Th65;
hence (- f) .: X is bounded_below by A1, Lm2; :: according to MEASURE6:def 5,MEASURE6:def 13 :: thesis: lower_bound ((- f) .: X) in (- f) .: X
then A4: lower_bound ((- f) .: X) = - (upper_bound (-- (-- (f .: X)))) by A3, Th43
.= - (upper_bound (f .: X)) ;
- (upper_bound (f .: X)) in -- (f .: X) by A2;
hence lower_bound ((- f) .: X) in (- f) .: X by A4, Th65; :: thesis: verum