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;
A1: z is Element of NAT by ORDINAL1:def 13;
consider f being IL-Function of NAT , STC N such that
A2: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & il. (STC N),z = f . z ) by Def12;
reconsider f2 = id NAT as IL-Function of NAT , STC N by AMI_1:def 36;

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: ( f2 . (k + 1) = k + 1 & f2 . k = k ) by FUNCT_1:35;
A4: SUCC (f2 . k) = {k,(k + 1)} by Th24, 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 )
assume A5: f2 . j in SUCC (f2 . k) ; :: thesis: k <= j
( j = f2 . j & j + 1 = f2 . (j + 1) ) by FUNCT_1:35;
then ( j = k or j = k + 1 ) by A4, A5, 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 f = f2 by A2, Th17;
hence il. (STC N),z = z by A1, A2, FUNCT_1:35; :: thesis: verum