theorem Th35: :: SCMRING3:36
for R being Ring
for k being Nat holds
( k + 1 in SUCC (k,(SCM R)) & ( for j being Nat st j in SUCC (k,(SCM R)) holds
k <= j ) )