set M = STC N;
reconsider f = id NAT as IL-Function of NAT , STC N by AMI_1:def 36;

now

let k be Element of NAT ; :: thesis: ( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) )
A1: ( f . (k + 1) = k + 1 & SUCC (f . k) = {k,(k + 1)} ) by Th24, FUNCT_1:35;
hence f . (k + 1) in SUCC (f . k) by TARSKI:def 2; :: thesis: for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j
let j be Element of NAT ; :: thesis: ( f . j in SUCC (f . k) implies k <= j )
assume f . j in SUCC (f . k) ; :: thesis: k <= j
then ( f . j = k or f . j = k + 1 ) by A1, TARSKI:def 2;
then ( j = k + 1 or j = k ) by FUNCT_1:35;
hence k <= j by NAT_1:11; :: thesis: verum

end;

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