let T be TopStruct ; :: thesis: for f being RealMap of T st f is continuous holds
- f is continuous
let f be RealMap of T; :: thesis: ( f is continuous implies - f is continuous )
assume A1: f is continuous ; :: thesis: - f is continuous
let X be Subset of REAL ; :: according to PSCOMP_1:def 25 :: thesis: ( X is closed implies (- f) " X is closed )
assume X is closed ; :: thesis: (- f) " X is closed
then A2: - X is closed by Th19;
(- f) " X = f " (- X) by Th43;
hence (- f) " X is closed by A1, A2, Def25; :: thesis: verum