let T be non empty TopSpace; :: thesis: ( ( for f being RealMap of T st f is continuous holds
f is with_max ) iff for f being RealMap of T st f is continuous holds
f is with_min )
hereby :: thesis: ( ( for f being RealMap of T st f is continuous holds
f is with_min ) implies for f being RealMap of T st f is continuous holds
f is with_max )
assume A1: for f being RealMap of T st f is continuous holds
f is with_max ; :: thesis: for f being RealMap of T st f is continuous holds
f is with_min
let f be RealMap of T; :: thesis: ( f is continuous implies f is with_min )
assume f is continuous ; :: thesis: f is with_min
then - f is continuous by Th9;
then - f is with_max by A1;
hence f is with_min by MEASURE6:66; :: thesis: verum
end;
assume A2: for f being RealMap of T st f is continuous holds
f is with_min ; :: thesis: for f being RealMap of T st f is continuous holds
f is with_max
let f be RealMap of T; :: thesis: ( f is continuous implies f is with_max )
assume f is continuous ; :: thesis: f is with_max
then - f is continuous by Th9;
then - (- f) is with_max by A2, Lm2;
hence f is with_max ; :: thesis: verum