let X be set ; :: thesis: for h being PartFunc of , st h | X is non-decreasing holds
(- h) | X is non-increasing
let h be PartFunc of ,; :: 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