let k be Element of NAT ; :: thesis: ( k + 1 in SUCC k,SCM+FSA & ( for j being Element of NAT st j in SUCC k,SCM+FSA holds
k <= j ) )
A11: SUCC k,SCM+FSA = {k,(succ k)} by Th84;
hence k + 1 in SUCC k,SCM+FSA by TARSKI:def 2; :: thesis: for j being Element of NAT st j in SUCC k,SCM+FSA holds
k <= j
let j be Element of NAT ; :: thesis: ( j in SUCC k,SCM+FSA implies k <= j )
assume A13: j in SUCC k,SCM+FSA ; :: thesis: k <= j

per cases ( j = k or j = succ k ) by A11, A13, TARSKI:def 2;

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

hence k <= j ; :: thesis: verum

end;

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

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

end;

end;