theorem :: RFUNCT_2:27

for X, Y being set
for h being PartFunc of REAL,REAL st h | Y is non-decreasing & h | X is non-increasing holds
h | (Y /\ X) is constant