let k be natural number ; :: thesis: succ (il. SCM ,k) = il. SCM ,(k + 1)
thus succ (il. SCM ,k) = succ k by Th54
.= k + 1
.= il. SCM ,(k + 1) by Th54 ; :: thesis: verum