set M = STC N;
now 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 ) )let k be
Nat;
( 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;
for j being Nat st j in SUCC (k,(STC N)) holds
k <= jlet j be
Nat;
( j in SUCC (k,(STC N)) implies k <= j )assume
j in SUCC (
k,
(STC N))
;
k <= jthen
(
j = k or
j = k + 1 )
by A1, TARSKI:def 2;
hence
k <= j
by NAT_1:11;
verum end;
hence
STC N is standard
by Th3; verum