reconsider f = id NAT as Function of NAT ,NAT ;
set M = STC N;
now let k be
Element of
NAT ;
( f . (k + 1) in SUCC (f . k),(STC N) & ( for j being Element of NAT st f . j in SUCC (f . k),(STC N) holds
k <= j ) )reconsider fk =
f . k as
Element of
NAT ;
A1:
SUCC fk,
(STC N) = {k,(k + 1)}
by Th24, FUNCT_1:35;
f . (k + 1) = k + 1
by FUNCT_1:35;
hence
f . (k + 1) in SUCC (f . k),
(STC N)
by A1, TARSKI:def 2;
for j being Element of NAT st f . j in SUCC (f . k),(STC N) holds
k <= jlet j be
Element of
NAT ;
( f . j in SUCC (f . k),(STC N) implies k <= j )assume
f . j in SUCC (f . k),
(STC N)
;
k <= jthen
(
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;
verum end;
hence
STC N is standard
by Th19; verum