let k be Nat; :: thesis: ( k + 1 in SUCC (k,SCM+FSA) & ( for j being Nat st j in SUCC (k,SCM+FSA) holds
k <= j ) )
A1: SUCC (k,SCM+FSA) = {k,(k + 1)} by Th39;
hence k + 1 in SUCC (k,SCM+FSA) by TARSKI:def 2; :: thesis: for j being Nat st j in SUCC (k,SCM+FSA) holds
k <= j
let j be Nat; :: thesis: ( j in SUCC (k,SCM+FSA) implies k <= j )
assume A2: j in SUCC (k,SCM+FSA) ; :: thesis: k <= j
per cases ( j = k or j = k + 1 ) by A1, A2, TARSKI:def 2;
suppose j = k ; :: thesis: k <= j
hence k <= j ; :: thesis: verum
end;
suppose j = k + 1 ; :: thesis: k <= j
hence k <= j by NAT_1:11; :: thesis: verum
end;
end;