theorem Th18: :: SCMPDS_9:18

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