set IR9 = the InternalRel of (OrderedNAT \~);
set CR9 = the carrier of (OrderedNAT \~);

now :: thesis: for N being set st N c= the carrier of (OrderedNAT \~) & N <> {} holds
ex m being object st
( m in N & the InternalRel of (OrderedNAT \~) -Seg m misses N )

let N be set ; :: thesis: ( N c= the carrier of (OrderedNAT \~) & N <> {} implies ex m being object st
( m in N & the InternalRel of (OrderedNAT \~) -Seg m misses N ) )
assume that
A1: N c= the carrier of (OrderedNAT \~) and
A2: N <> {} ; :: thesis: ex m being object st
( m in N & the InternalRel of (OrderedNAT \~) -Seg m misses N )
A3: ex k being object st k in N by A2, XBOOLE_0:def 1;
defpred S₁[ Nat] means c₁ in N;
A4: ex k being Nat st S₁[k] by A1, A3;
consider m being Nat such that
A5: S₁[m] and
A6: for n being Nat st S₁[n] holds
m <= n from NAT_1:sch 5(A4);
reconsider m = m as Element of OrderedNAT by ORDINAL1:def 12;
thus ex m being object st
( m in N & the InternalRel of (OrderedNAT \~) -Seg m misses N ) :: thesis: verum

proof

take m ; :: thesis: ( m in N & the InternalRel of (OrderedNAT \~) -Seg m misses N )
thus m in N by A5; :: thesis: the InternalRel of (OrderedNAT \~) -Seg m misses N

now :: thesis: not ( the InternalRel of (OrderedNAT \~) -Seg m) /\ N <> {}

assume ( the InternalRel of (OrderedNAT \~) -Seg m) /\ N <> {} ; :: thesis: contradiction
then consider z being object such that
A7: z in ( the InternalRel of (OrderedNAT \~) -Seg m) /\ N by XBOOLE_0:def 1;
A8: z in the InternalRel of (OrderedNAT \~) -Seg m by A7, XBOOLE_0:def 4;
A9: z in N by A7, XBOOLE_0:def 4;
A10: z <> m by A8, WELLORD1:1;
A11: [z,m] in the InternalRel of (OrderedNAT \~) by A8, WELLORD1:1;
then [z,m] in NATOrd ;
then consider x, y being Element of NAT such that
A12: [z,m] = [x,y] and
x <= y ;
A13: z = x by A12, XTUPLE_0:1;
A14: m = y by A12, XTUPLE_0:1;
then y <= x by A6, A9, A13;
then [y,x] in NATOrd ;
hence contradiction by A10, A11, A13, A14, Th43; :: thesis: verum

end;

hence the InternalRel of (OrderedNAT \~) -Seg m misses N by XBOOLE_0:def 7; :: thesis: verum

end;

end;

then the InternalRel of (OrderedNAT \~) is_well_founded_in the carrier of (OrderedNAT \~) by WELLORD1:def 3;
then OrderedNAT \~ is well_founded by WELLFND1:def 2;
hence OrderedNAT is Dickson by Th26; :: thesis: verum