set IR' = the InternalRel of (OrderedNAT \~ );
set CR' = the carrier of (OrderedNAT \~ );
now let N be
set ;
:: thesis: ( 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 <> {}
;
:: thesis: ex m being set st
( m in N & the InternalRel of (OrderedNAT \~ ) -Seg m misses N )consider k being
set such that A3:
k in N
by A2, XBOOLE_0:def 1;
defpred S1[
Nat]
means c1 in N;
ex
k being
Element of
NAT st
S1[
k]
by A1, A3;
then A4:
ex
k being
Nat st
S1[
k]
;
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 )
:: thesis: verumproof
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 assume
(the InternalRel of (OrderedNAT \~ ) -Seg m) /\ N <> {}
;
:: thesis: 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 &
z in N )
by A7, XBOOLE_0:def 4;
then A9:
(
z <> m &
[z,m] in the
InternalRel of
(OrderedNAT \~ ) )
by WELLORD1:def 1;
then
[z,m] in NATOrd
;
then consider x,
y being
Element of
NAT such that A10:
[z,m] = [x,y]
and
x <= y
;
A11:
(
z = x &
m = y )
by A10, ZFMISC_1:33;
then
y <= x
by A6, A8;
then
[y,x] in NATOrd
;
hence
contradiction
by A9, A11, Th45, RELAT_2:def 4;
:: 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 Th28; :: thesis: verum