set M = STC N;

now :: thesis: for k being Nat holds

( k + 1 in SUCC (k,(STC N)) & ( for j being Nat st j in SUCC (k,(STC N)) holds

k <= j ) )

hence
STC N is standard
by Th3; :: thesis: verum( k + 1 in SUCC (k,(STC N)) & ( for j being Nat st j in SUCC (k,(STC N)) holds

k <= j ) )

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

k <= j ) )

A1: SUCC (k,(STC N)) = {k,(k + 1)} by Th8;

thus k + 1 in SUCC (k,(STC N)) by A1, TARSKI:def 2; :: thesis: for j being Nat st j in SUCC (k,(STC N)) holds

k <= j

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

assume j in SUCC (k,(STC N)) ; :: thesis: k <= j

then ( j = k or j = k + 1 ) by A1, TARSKI:def 2;

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

end;k <= j ) )

A1: SUCC (k,(STC N)) = {k,(k + 1)} by Th8;

thus k + 1 in SUCC (k,(STC N)) by A1, TARSKI:def 2; :: thesis: for j being Nat st j in SUCC (k,(STC N)) holds

k <= j

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

assume j in SUCC (k,(STC N)) ; :: thesis: k <= j

then ( j = k or j = k + 1 ) by A1, TARSKI:def 2;

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