set IR9 = the InternalRel of (OrderedNAT \~);
set CR9 = the carrier of (OrderedNAT \~);
now let N be
set ;
( N c= the carrier of (OrderedNAT \~) & N <> {} implies ex m being set st
( m in N & the InternalRel of (OrderedNAT \~) -Seg m misses N ) )assume that A1:
N c= the
carrier of
(OrderedNAT \~)
and A2:
N <> {}
;
ex m being set st
( m in N & the InternalRel of (OrderedNAT \~) -Seg m misses N )A3:
ex
k being
set st
k in N
by A2, XBOOLE_0:def 1;
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 NAT_1:sch 5(A4);
reconsider m =
m as
Element of
OrderedNAT by ORDINAL1:def 13;
thus
ex
m being
set st
(
m in N & the
InternalRel of
(OrderedNAT \~) -Seg m misses N )
verumproof
take
m
;
( m in N & the InternalRel of (OrderedNAT \~) -Seg m misses N )
thus
m in N
by A5;
the InternalRel of (OrderedNAT \~) -Seg m misses N
now assume
( the InternalRel of (OrderedNAT \~) -Seg m) /\ N <> {}
;
contradictionthen consider z being
set 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:def 1;
A11:
[z,m] in the
InternalRel of
(OrderedNAT \~)
by A8, WELLORD1:def 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, ZFMISC_1:33;
A14:
m = y
by A12, ZFMISC_1:33;
then
y <= x
by A6, A9, A13;
then
[y,x] in NATOrd
;
hence
contradiction
by A10, A11, A13, A14, Th45, RELAT_2:def 4;
verum end;
hence
the
InternalRel of
(OrderedNAT \~) -Seg m misses N
by XBOOLE_0:def 7;
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 Th28; verum