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