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

k <= j ) )

reconsider fk = k as Element of NAT by ORDINAL1:def 12;

A1: SUCC (k,SCM) = {k,(fk + 1)} by Th21;

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

k <= j

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

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

reconsider fk = k as Element of NAT by ORDINAL1:def 12;

k <= j ) )

reconsider fk = k as Element of NAT by ORDINAL1:def 12;

A1: SUCC (k,SCM) = {k,(fk + 1)} by Th21;

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

k <= j

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

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

reconsider fk = k as Element of NAT by ORDINAL1:def 12;