theorem Th34: :: SCMRING3:35

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