theorem Th40: :: SCMFSA10:40

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