let z be natural number ; :: thesis: for N being with_non-empty_elements set holds il. (STC N),z = z
let N be with_non-empty_elements set ; :: thesis: il. (STC N),z = z
set M = STC N;
reconsider f2 = id NAT as IL-Function of NAT , STC N by AMI_1:def 36;
consider f being IL-Function of NAT , STC N such that
A1: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . 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) & ( for j being Element of NAT st f2 . j in SUCC (f2 . k) holds
k <= j ) )
A3: SUCC (f2 . k) = {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) by A3, TARSKI:def 2; :: thesis: for j being Element of NAT st f2 . j in SUCC (f2 . k) holds
k <= j
let j be Element of NAT ; :: thesis: ( f2 . j in SUCC (f2 . k) implies k <= j )
A4: j = f2 . j by FUNCT_1:35;
assume f2 . j in SUCC (f2 . k) ; :: 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 ) 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