theorem :: RFUNCT_2:47

for R being Subset of REAL holds (id R) | R is increasing