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 AMISTD_1:8, FUNCT_1:18;
f2 . (k + 1) = k + 1 by FUNCT_1:18;
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:18;
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 12;
hence il. ((STC N),z) = z by A2, FUNCT_1:18; :: thesis: verum