theorem Th22: :: AMI_6:22

for k being Nat holds
( k + 1 in SUCC (k,SCM) & ( for j being Nat st j in SUCC (k,SCM) holds
k <= j ) )