let X be non empty set ; :: thesis: for f being Function of X,REAL st f is with_min holds
- f is with_max
let f be Function of X,REAL ; :: thesis: ( f is with_min implies - f is with_max )
assume that
A1: f .: X is bounded_below and
A2: inf (f .: X) in f .: X ; :: according to PSCOMP_1:def 4,PSCOMP_1:def 15 :: thesis: - f is with_max
A3: - (f .: X) = (- f) .: X by Th40;
hence A4: (- f) .: X is bounded_above by A1, Lm2; :: according to PSCOMP_1:def 3,PSCOMP_1:def 14 :: thesis: sup ((- f) .: X) in (- f) .: X
A5: - (inf (f .: X)) in - (f .: X) by A2;
sup ((- f) .: X) = - (inf (- (- (f .: X)))) by A3, A4, Th18
.= - (inf (f .: X)) ;
hence sup ((- f) .: X) in (- f) .: X by A5, Th40; :: thesis: verum