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