set IR9 = the InternalRel of ();
set CR9 = the carrier of ();
now :: thesis: for N being set st N c= the carrier of () & N <> {} holds
ex m being object st
( m in N & the InternalRel of () -Seg m misses N )
let N be set ; :: thesis: ( N c= the carrier of () & N <> {} implies ex m being object st
( m in N & the InternalRel of () -Seg m misses N ) )

assume that
A1: N c= the carrier of () and
A2: N <> {} ; :: thesis: ex m being object st
( m in N & the InternalRel of () -Seg m misses N )

A3: ex k being object st k in N by ;
defpred S1[ Nat] means c1 in N;
A4: ex k being Nat st S1[k] by A1, A3;
consider m being Nat such that
A5: S1[m] and
A6: for n being Nat st S1[n] holds
m <= n from reconsider m = m as Element of OrderedNAT by ORDINAL1:def 12;
thus ex m being object st
( m in N & the InternalRel of () -Seg m misses N ) :: thesis: verum
proof
take m ; :: thesis: ( m in N & the InternalRel of () -Seg m misses N )
thus m in N by A5; :: thesis: the InternalRel of () -Seg m misses N
now :: thesis: not ( the InternalRel of () -Seg m) /\ N <> {}
assume ( the InternalRel of () -Seg m) /\ N <> {} ; :: thesis: contradiction
then consider z being object such that
A7: z in ( the InternalRel of () -Seg m) /\ N by XBOOLE_0:def 1;
A8: z in the InternalRel of () -Seg m by ;
A9: z in N by ;
A10: z <> m by ;
A11: [z,m] in the InternalRel of () by ;
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 ;
A14: m = y by ;
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 () -Seg m misses N by XBOOLE_0:def 7; :: thesis: verum
end;
end;
then the InternalRel of () is_well_founded_in the carrier of () by WELLORD1:def 3;
then OrderedNAT \~ is well_founded by WELLFND1:def 2;
hence OrderedNAT is Dickson by Th26; :: thesis: verum