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

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

then OrderedNAT \~ is well_founded by WELLFND1:def 2;

hence OrderedNAT is Dickson by Th26; :: thesis: verum

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 )

then
the InternalRel of (OrderedNAT \~) is_well_founded_in the carrier of (OrderedNAT \~)
by WELLORD1:def 3;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_{1}[ Nat] means c_{1} in N;

A4: ex k being Nat st S_{1}[k]
by A1, A3;

consider m being Nat such that

A5: S_{1}[m]
and

A6: for n being Nat st S_{1}[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

end;( 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

A4: ex k being Nat st S

consider m being Nat such that

A5: S

A6: for n being Nat st S

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

end;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 <> {}

hence
the InternalRel of (OrderedNAT \~) -Seg m misses N
by XBOOLE_0:def 7; :: thesis: verumassume
( 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;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

then OrderedNAT \~ is well_founded by WELLFND1:def 2;

hence OrderedNAT is Dickson by Th26; :: thesis: verum