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