let R be good Ring; :: thesis: for k being Element of NAT holds
( k + 1 in SUCC k,(SCM R) & ( for j being Element of NAT st j in SUCC k,(SCM R) holds
k <= j ) )
let k be Element of NAT ; :: thesis: ( k + 1 in SUCC k,(SCM R) & ( for j being Element of NAT st j in SUCC k,(SCM R) holds
k <= j ) )
reconsider fk = k as Element of NAT ;
A7: SUCC k,(SCM R) = {k,(succ fk)} by Th64;
hence k + 1 in SUCC k,(SCM R) by TARSKI:def 2; :: thesis: for j being Element of NAT st j in SUCC k,(SCM R) holds
k <= j
let j be Element of NAT ; :: thesis: ( j in SUCC k,(SCM R) implies k <= j )
assume A9: j in SUCC k,(SCM R) ; :: thesis: k <= j
reconsider fk = k as Element of NAT ;

per cases ( j = k or j = succ fk ) by A7, A9, TARSKI:def 2;

suppose j = k ; :: thesis: k <= j

hence k <= j ; :: thesis: verum

end;

suppose j = succ fk ; :: thesis: k <= j

hence k <= j by NAT_1:11; :: thesis: verum

end;

end;