theorem :: RFUNCT_2:49

for X being set
for h being PartFunc of REAL,REAL st h | X is non-decreasing holds
(- h) | X is non-increasing by Th34;