set M = STC N;

now

let k be Element of NAT ; :: thesis: ( k + 1 in SUCC (k,(STC N)) & ( for j being Element of NAT st j in SUCC (k,(STC N)) holds
k <= j ) )
A1: SUCC (k,(STC N)) = {k,(k + 1)} by Th24;
thus k + 1 in SUCC (k,(STC N)) by A1, TARSKI:def 2; :: thesis: for j being Element of NAT st j in SUCC (k,(STC N)) holds
k <= j
let j be Element of 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;

hence STC N is standard by Th19; :: thesis: verum