let R be Ring; :: thesis: 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 ) )

let k be Nat; :: thesis: ( k + 1 in SUCC (k,(SCM R)) & ( for j being Nat st j in SUCC (k,(SCM R)) holds

k <= j ) )

A1: SUCC (k,(SCM R)) = {k,(k + 1)} by Th34;

hence k + 1 in SUCC (k,(SCM R)) by TARSKI:def 2; :: thesis: for j being Nat st j in SUCC (k,(SCM R)) holds

k <= j

let j be Nat; :: thesis: ( j in SUCC (k,(SCM R)) implies k <= j )

assume A2: j in SUCC (k,(SCM R)) ; :: thesis: k <= j

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

k <= j ) )

let k be Nat; :: thesis: ( k + 1 in SUCC (k,(SCM R)) & ( for j being Nat st j in SUCC (k,(SCM R)) holds

k <= j ) )

A1: SUCC (k,(SCM R)) = {k,(k + 1)} by Th34;

hence k + 1 in SUCC (k,(SCM R)) by TARSKI:def 2; :: thesis: for j being Nat st j in SUCC (k,(SCM R)) holds

k <= j

let j be Nat; :: thesis: ( j in SUCC (k,(SCM R)) implies k <= j )

assume A2: j in SUCC (k,(SCM R)) ; :: thesis: k <= j