theorem Th21: :: AMI_6:21

for il being Nat holds SUCC (il,SCM) = {il,(il + 1)}