let z be natural number ; :: thesis: for N being non empty with_non-empty_elements set holds il. (STC N),z = z
let N be non empty with_non-empty_elements set ; :: thesis: il. (STC N),z = z
set M = STC N;
reconsider f2 = id NAT as Function of NAT ,NAT ;
consider f being Function of NAT ,NAT such that
A1: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n, STC N ) ) ) and
A2: il. (STC N),z = f . z by Def12;

now

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

end;

then for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n, STC N ) by Th18;
then ( z is Element of NAT & f = f2 ) by A1, Th17, ORDINAL1:def 13;
hence il. (STC N),z = z by A2, FUNCT_1:35; :: thesis: verum