for X being set
for f being PartFunc of REAL,REAL st ( f | X is increasing or f | X is decreasing ) holds
f | X is one-to-one