theorem Th9: :: FCONT_3:9

for X being set
for f being one-to-one PartFunc of REAL,REAL st f | X is increasing holds
((f | X) ") | (f .: X) is increasing