for l being Element of NAT holds SUCC (l,SCMPDS) = NAT