let X be set ; :: thesis: for h being PartFunc of REAL,REAL st h | X is increasing holds
(- h) | X is decreasing
let h be PartFunc of REAL,REAL; :: thesis: ( h | X is increasing implies (- h) | X is decreasing )
assume h | X is increasing ; :: thesis: (- h) | X is decreasing
then ((- 1) (#) h) | X is decreasing by Th64;
hence (- h) | X is decreasing ; :: thesis: verum