theorem :: FRECHET2:2

for RS being Real_Sequence st RS = id NAT holds
RS is increasing sequence of NAT ;