:: Dickson's lemma
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received March 12, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users

theorem Th1: :: DICKSON:1

for g being Function
for x being set st dom g = {x} holds
g = x .--> (g . x)

proof end;

theorem :: DICKSON:2

canceled;

::$CT

theorem Th2: :: DICKSON:3

for X being infinite set ex f being sequence of X st f is one-to-one

proof end;

definition

let R be RelStr ;
let f be sequence of R;

attr f is ascending means :: DICKSON:def 1
for n being Element of NAT holds
( f . (n + 1) <> f . n & [(f . n),(f . (n + 1))] in the InternalRel of R );

end;

:: deftheorem defines ascending DICKSON:def 1 :
for R being RelStr
for f being sequence of R holds
( f is ascending iff for n being Element of NAT holds
( f . (n + 1) <> f . n & [(f . n),(f . (n + 1))] in the InternalRel of R ) );

definition

let R be RelStr ;
let f be sequence of R;

attr f is weakly-ascending means :: DICKSON:def 2
for n being Nat holds [(f . n),(f . (n + 1))] in the InternalRel of R;

end;

:: deftheorem defines weakly-ascending DICKSON:def 2 :
for R being RelStr
for f being sequence of R holds
( f is weakly-ascending iff for n being Nat holds [(f . n),(f . (n + 1))] in the InternalRel of R );

theorem Th3: :: DICKSON:4

for R being non empty transitive RelStr
for f being sequence of R st f is weakly-ascending holds
for i, j being Nat st i < j holds
f . i <= f . j

proof end;

theorem Th4: :: DICKSON:5

for R being non empty RelStr holds
( R is connected iff the InternalRel of R is_strongly_connected_in the carrier of R )

proof end;

theorem Th5: :: DICKSON:6

for L being RelStr
for Y, a being set holds
( ( the InternalRel of L -Seg a misses Y & a in Y ) iff a is_minimal_wrt Y, the InternalRel of L )

proof end;

theorem Th6: :: DICKSON:7

for L being non empty transitive antisymmetric RelStr
for x being Element of L
for a, N being set st a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L holds
a is_minimal_wrt N, the InternalRel of L

proof end;

definition

let R be RelStr ;

attr R is quasi_ordered means :: DICKSON:def 3
( R is reflexive & R is transitive );

end;

:: deftheorem defines quasi_ordered DICKSON:def 3 :
for R being RelStr holds
( R is quasi_ordered iff ( R is reflexive & R is transitive ) );

definition

let R be RelStr ;
assume A1: R is quasi_ordered ;

func EqRel R -> Equivalence_Relation of the carrier of R equals :Def4: :: DICKSON:def 4
the InternalRel of R /\ ( the InternalRel of R ~);

coherence
the InternalRel of R /\ ( the InternalRel of R ~) is Equivalence_Relation of the carrier of R

proof end;

end;

:: deftheorem Def4 defines EqRel DICKSON:def 4 :
for R being RelStr st R is quasi_ordered holds
EqRel R = the InternalRel of R /\ ( the InternalRel of R ~);

theorem Th7: :: DICKSON:8

for R being RelStr
for x, y being Element of R st R is quasi_ordered holds
( x in Class ((EqRel R),y) iff ( x <= y & y <= x ) )

proof end;

definition

let R be RelStr ;

func <=E R -> Relation of (Class (EqRel R)) means :Def5: :: DICKSON:def 5
for A, B being object holds
( [A,B] in it iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) );

existence
ex b₁ being Relation of (Class (EqRel R)) st
for A, B being object holds
( [A,B] in b₁ iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )

proof end;

uniqueness
for b₁, b₂ being Relation of (Class (EqRel R)) st ( for A, B being object holds
( [A,B] in b₁ iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) & ( for A, B being object holds
( [A,B] in b₂ iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines <=E DICKSON:def 5 :
for R being RelStr
for b₂ being Relation of (Class (EqRel R)) holds
( b₂ = <=E R iff for A, B being object holds
( [A,B] in b₂ iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) );

theorem Th8: :: DICKSON:9

for R being RelStr st R is quasi_ordered holds
<=E R partially_orders Class (EqRel R)

proof end;

theorem :: DICKSON:10

for R being non empty RelStr st R is quasi_ordered & R is connected holds
<=E R linearly_orders Class (EqRel R)

proof end;

definition

let R be Relation;

func R \~ -> Relation equals :: DICKSON:def 6
R \ (R ~);

correctness
coherence
R \ (R ~) is Relation;
;

end;

:: deftheorem defines \~ DICKSON:def 6 :
for R being Relation holds R \~ = R \ (R ~);

registration

let R be Relation;

cluster R \~ -> asymmetric ;

coherence
R \~ is asymmetric

proof end;

end;

definition

let X be set ;
let R be Relation of X;
:: original: \~
redefine func R \~ -> Relation of X;
coherence
R \~ is Relation of X

proof end;

end;

definition

let R be RelStr ;

func R \~ -> strict RelStr equals :: DICKSON:def 7
RelStr(# the carrier of R,( the InternalRel of R \~) #);

correctness
coherence
RelStr(# the carrier of R,( the InternalRel of R \~) #) is strict RelStr ;
;

end;

:: deftheorem defines \~ DICKSON:def 7 :
for R being RelStr holds R \~ = RelStr(# the carrier of R,( the InternalRel of R \~) #);

registration

let R be non empty RelStr ;

cluster R \~ -> non empty strict ;

coherence
not R \~ is empty ;

end;

registration

let R be transitive RelStr ;

cluster R \~ -> strict transitive ;

coherence
R \~ is transitive

proof end;

end;

registration

let R be RelStr ;

cluster R \~ -> strict antisymmetric ;

coherence
R \~ is antisymmetric

proof end;

end;

theorem :: DICKSON:11

for R being non empty Poset
for x being Element of R holds Class ((EqRel R),x) = {x}

proof end;

theorem :: DICKSON:12

for R being Relation holds
( R = R \~ iff R is asymmetric )

proof end;

theorem :: DICKSON:13

for R being Relation st R is transitive holds
R \~ is transitive

proof end;

theorem :: DICKSON:14

for R being Relation
for a, b being set st R is antisymmetric holds
( [a,b] in R \~ iff ( [a,b] in R & a <> b ) )

proof end;

theorem Th14: :: DICKSON:15

for R being RelStr st R is well_founded holds
R \~ is well_founded

proof end;

theorem Th15: :: DICKSON:16

for R being RelStr st R \~ is well_founded & R is antisymmetric holds
R is well_founded

proof end;

theorem Th16: :: DICKSON:17

for L being RelStr
for N being set
for x being Element of (L \~) holds
( x is_minimal_wrt N, the InternalRel of (L \~) iff ( x in N & ( for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of L ) ) )

proof end;

:: Proposition 4.31 - see WELLFND1:15
:: Omitting Example 4.32, Exercise 4.33, Exercise 4.34

theorem :: DICKSON:18

for R, S being non empty RelStr
for m being Function of R,S st R is quasi_ordered & S is antisymmetric & S \~ is well_founded & ( for a, b being Element of R holds
( ( a <= b implies m . a <= m . b ) & ( m . a = m . b implies [a,b] in EqRel R ) ) ) holds
R \~ is well_founded

proof end;

definition

let R be non empty RelStr ;
let N be Subset of R;

func min-classes N -> Subset-Family of R means :Def8: :: DICKSON:def 8
for x being set holds
( x in it iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) );

existence
ex b₁ being Subset-Family of R st
for x being set holds
( x in b₁ iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of R st ( for x being set holds
( x in b₁ iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) ) & ( for x being set holds
( x in b₂ iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines min-classes DICKSON:def 8 :
for R being non empty RelStr
for N being Subset of R
for b₃ being Subset-Family of R holds
( b₃ = min-classes N iff for x being set holds
( x in b₃ iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) );

theorem Th18: :: DICKSON:19

for R being non empty RelStr
for N being Subset of R
for x being set st R is quasi_ordered & x in min-classes N holds
for y being Element of (R \~) st y in x holds
y is_minimal_wrt N, the InternalRel of (R \~)

proof end;

theorem Th19: :: DICKSON:20

for R being non empty RelStr holds
( R \~ is well_founded iff for N being Subset of R st N <> {} holds
ex x being object st x in min-classes N )

proof end;

theorem Th20: :: DICKSON:21

for R being non empty RelStr
for N being Subset of R
for y being Element of (R \~) st y is_minimal_wrt N, the InternalRel of (R \~) holds
not min-classes N is empty

proof end;

theorem Th21: :: DICKSON:22

for R being non empty RelStr
for N being Subset of R
for x being set st x in min-classes N holds
not x is empty

proof end;

theorem Th22: :: DICKSON:23

for R being non empty RelStr st R is quasi_ordered holds
( ( R is connected & R \~ is well_founded ) iff for N being non empty Subset of R holds card (min-classes N) = 1 )

proof end;

theorem :: DICKSON:24

for R being non empty Poset holds
( the InternalRel of R well_orders the carrier of R iff for N being non empty Subset of R holds card (min-classes N) = 1 )

proof end;

definition

let R be RelStr ;
let N be Subset of R;
let B be set ;

pred B is_Dickson-basis_of N,R means :: DICKSON:def 9
( B c= N & ( for a being Element of R st a in N holds
ex b being Element of R st
( b in B & b <= a ) ) );

end;

:: deftheorem defines is_Dickson-basis_of DICKSON:def 9 :
for R being RelStr
for N being Subset of R
for B being set holds
( B is_Dickson-basis_of N,R iff ( B c= N & ( for a being Element of R st a in N holds
ex b being Element of R st
( b in B & b <= a ) ) ) );

theorem :: DICKSON:25

for R being RelStr holds {} is_Dickson-basis_of {} the carrier of R,R ;

theorem Th25: :: DICKSON:26

for R being non empty RelStr
for N being non empty Subset of R
for B being set st B is_Dickson-basis_of N,R holds
not B is empty

proof end;

definition

let R be RelStr ;

attr R is Dickson means :: DICKSON:def 10
for N being Subset of R ex B being set st
( B is_Dickson-basis_of N,R & B is finite );

end;

:: deftheorem defines Dickson DICKSON:def 10 :
for R being RelStr holds
( R is Dickson iff for N being Subset of R ex B being set st
( B is_Dickson-basis_of N,R & B is finite ) );

theorem Th26: :: DICKSON:27

for R being non empty RelStr st R \~ is well_founded & R is connected holds
R is Dickson

proof end;

theorem Th27: :: DICKSON:28

for R, S being RelStr st the InternalRel of R c= the InternalRel of S & R is Dickson & the carrier of R = the carrier of S holds
S is Dickson

proof end;

definition

let f be Function;
let b be set ;
assume that
A1: dom f = NAT and
A2: b in rng f ;

func f mindex b -> Element of NAT means :Def11: :: DICKSON:def 11
( f . it = b & ( for i being Element of NAT st f . i = b holds
it <= i ) );

existence
ex b₁ being Element of NAT st
( f . b₁ = b & ( for i being Element of NAT st f . i = b holds
b₁ <= i ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st f . b₁ = b & ( for i being Element of NAT st f . i = b holds
b₁ <= i ) & f . b₂ = b & ( for i being Element of NAT st f . i = b holds
b₂ <= i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines mindex DICKSON:def 11 :
for f being Function
for b being set st dom f = NAT & b in rng f holds
for b₃ being Element of NAT holds
( b₃ = f mindex b iff ( f . b₃ = b & ( for i being Element of NAT st f . i = b holds
b₃ <= i ) ) );

definition

let R be non empty 1-sorted ;
let f be sequence of R;
let b be set ;
let m be Element of NAT ;
assume A1: ex j being Element of NAT st
( m < j & f . j = b ) ;

func f mindex (b,m) -> Element of NAT means :Def12: :: DICKSON:def 12
( f . it = b & m < it & ( for i being Element of NAT st m < i & f . i = b holds
it <= i ) );

existence
ex b₁ being Element of NAT st
( f . b₁ = b & m < b₁ & ( for i being Element of NAT st m < i & f . i = b holds
b₁ <= i ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st f . b₁ = b & m < b₁ & ( for i being Element of NAT st m < i & f . i = b holds
b₁ <= i ) & f . b₂ = b & m < b₂ & ( for i being Element of NAT st m < i & f . i = b holds
b₂ <= i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines mindex DICKSON:def 12 :
for R being non empty 1-sorted
for f being sequence of R
for b being set
for m being Element of NAT st ex j being Element of NAT st
( m < j & f . j = b ) holds
for b₅ being Element of NAT holds
( b₅ = f mindex (b,m) iff ( f . b₅ = b & m < b₅ & ( for i being Element of NAT st m < i & f . i = b holds
b₅ <= i ) ) );

theorem Th28: :: DICKSON:29

for R being non empty RelStr st R is Dickson holds
for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j )

proof end;

theorem Th29: :: DICKSON:30

for R being RelStr
for N being Subset of R
for x being Element of (R \~) st R is quasi_ordered & x in N & ( the InternalRel of R -Seg x) /\ N c= Class ((EqRel R),x) holds
x is_minimal_wrt N, the InternalRel of (R \~)

proof end;

theorem Th30: :: DICKSON:31

for R being non empty RelStr st R is quasi_ordered & ( for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j ) ) holds
for N being non empty Subset of R holds
( min-classes N is finite & not min-classes N is empty )

proof end;

theorem Th31: :: DICKSON:32

for R being non empty RelStr st R is quasi_ordered & ( for N being non empty Subset of R holds
( min-classes N is finite & not min-classes N is empty ) ) holds
R is Dickson

proof end;

theorem Th32: :: DICKSON:33

for R being non empty RelStr st R is quasi_ordered & R is Dickson holds
R \~ is well_founded

proof end;

theorem :: DICKSON:34

for R being non empty Poset
for N being non empty Subset of R st R is Dickson holds
ex B being set st
( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) )

proof end;

definition

let R be non empty RelStr ;
let N be Subset of R;
assume A1: R is Dickson ;

func Dickson-bases (N,R) -> non empty Subset-Family of R means :Def13: :: DICKSON:def 13
for B being set holds
( B in it iff B is_Dickson-basis_of N,R );

existence
ex b₁ being non empty Subset-Family of R st
for B being set holds
( B in b₁ iff B is_Dickson-basis_of N,R )

proof end;

uniqueness
for b₁, b₂ being non empty Subset-Family of R st ( for B being set holds
( B in b₁ iff B is_Dickson-basis_of N,R ) ) & ( for B being set holds
( B in b₂ iff B is_Dickson-basis_of N,R ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines Dickson-bases DICKSON:def 13 :
for R being non empty RelStr
for N being Subset of R st R is Dickson holds
for b₃ being non empty Subset-Family of R holds
( b₃ = Dickson-bases (N,R) iff for B being set holds
( B in b₃ iff B is_Dickson-basis_of N,R ) );

theorem Th34: :: DICKSON:35

for R being non empty RelStr
for s being sequence of R st R is Dickson holds
ex t being sequence of R st
( t is subsequence of s & t is weakly-ascending )

proof end;

theorem Th35: :: DICKSON:36

for R being RelStr st R is empty holds
R is Dickson

proof end;

theorem Th36: :: DICKSON:37

for M, N being RelStr st M is Dickson & N is Dickson & M is quasi_ordered & N is quasi_ordered holds
( [:M,N:] is quasi_ordered & [:M,N:] is Dickson )

proof end;

theorem Th37: :: DICKSON:38

for R, S being RelStr st R,S are_isomorphic & R is Dickson & R is quasi_ordered holds
( S is quasi_ordered & S is Dickson )

proof end;

theorem Th38: :: DICKSON:39

for p being RelStr-yielding ManySortedSet of {0}
for z being Element of {0} holds p . z, product p are_isomorphic

proof end;

registration

let X be set ;
let p be RelStr-yielding ManySortedSet of X;
let Y be Subset of X;

cluster p | Y -> RelStr-yielding ;

coherence
p | Y is RelStr-yielding

proof end;

end;

theorem Th39: :: DICKSON:40

for n being non zero Nat
for p being RelStr-yielding ManySortedSet of n holds
( not product p is empty iff p is non-Empty )

proof end;

theorem Th40: :: DICKSON:41

for n being non zero Nat
for p being RelStr-yielding ManySortedSet of Segm (n + 1)
for ns being Subset of (Segm (n + 1))
for ne being Element of Segm (n + 1) st ns = n & ne = n holds
[:(product (p | ns)),(p . ne):], product p are_isomorphic

proof end;

theorem Th41: :: DICKSON:42

for n being non zero Nat
for p being RelStr-yielding ManySortedSet of Segm n st ( for i being Element of Segm n holds
( p . i is Dickson & p . i is quasi_ordered ) ) holds
( product p is quasi_ordered & product p is Dickson )

proof end;

Lm1: for p being RelStr-yielding ManySortedSet of {} holds
( not product p is empty & product p is quasi_ordered & product p is Dickson & product p is antisymmetric )

proof end;

registration

let p be RelStr-yielding ManySortedSet of {} ;

cluster product p -> non empty ;

coherence
not product p is empty by Lm1;

cluster product p -> antisymmetric ;

coherence
product p is antisymmetric by Lm1;

cluster product p -> quasi_ordered ;

coherence
product p is quasi_ordered by Lm1;

cluster product p -> Dickson ;

coherence
product p is Dickson by Lm1;

end;

definition

::: RelIncl omega;

func NATOrd -> Relation of NAT equals :: DICKSON:def 14
{ [x,y] where x, y is Element of NAT : x <= y } ;

correctness
coherence
{ [x,y] where x, y is Element of NAT : x <= y } is Relation of NAT;

proof end;

end;

:: deftheorem defines NATOrd DICKSON:def 14 :
NATOrd = { [x,y] where x, y is Element of NAT : x <= y } ;

theorem Th42: :: DICKSON:43

NATOrd is_reflexive_in NAT ;

theorem Th43: :: DICKSON:44

NATOrd is_antisymmetric_in NAT

proof end;

theorem Th44: :: DICKSON:45

NATOrd is_strongly_connected_in NAT

proof end;

theorem Th45: :: DICKSON:46

NATOrd is_transitive_in NAT

proof end;

definition

func OrderedNAT -> non empty RelStr equals :: DICKSON:def 15
RelStr(# NAT,NATOrd #);

coherence
RelStr(# NAT,NATOrd #) is non empty RelStr ;

end;

:: deftheorem defines OrderedNAT DICKSON:def 15 :
OrderedNAT = RelStr(# NAT,NATOrd #);

Lm2: now :: thesis: OrderedNAT is connected

for x, y being Element of OrderedNAT st not x <= y holds
y <= x by Th44;
hence OrderedNAT is connected by WAYBEL_0:def 29; :: thesis: verum

end;

registration

cluster OrderedNAT -> non empty connected ;

coherence
OrderedNAT is connected by Lm2;

cluster OrderedNAT -> non empty Dickson ;

coherence
OrderedNAT is Dickson

proof end;

cluster OrderedNAT -> non empty quasi_ordered ;

coherence
OrderedNAT is quasi_ordered

proof end;

cluster OrderedNAT -> non empty antisymmetric ;

coherence
OrderedNAT is antisymmetric by Th43;

cluster OrderedNAT -> non empty transitive ;

coherence
OrderedNAT is transitive by Th45;

cluster OrderedNAT -> non empty well_founded ;

coherence
OrderedNAT is well_founded

proof end;

end;

Lm3: now :: thesis: for n being Element of NAT holds
( not product (n --> OrderedNAT) is empty & product (n --> OrderedNAT) is Dickson & product (n --> OrderedNAT) is quasi_ordered & product (n --> OrderedNAT) is antisymmetric )

let n be Element of NAT ; :: thesis: ( not product (b₁ --> OrderedNAT) is empty & product (b₁ --> OrderedNAT) is Dickson & product (b₁ --> OrderedNAT) is quasi_ordered & product (b₁ --> OrderedNAT) is antisymmetric )
set pp = product (n --> OrderedNAT);

per cases ( n is zero or not n is zero ) ;

suppose n is zero ; :: thesis: ( not product (b₁ --> OrderedNAT) is empty & product (b₁ --> OrderedNAT) is Dickson & product (b₁ --> OrderedNAT) is quasi_ordered & product (b₁ --> OrderedNAT) is antisymmetric )

then n = 0 ;
hence ( not product (n --> OrderedNAT) is empty & product (n --> OrderedNAT) is Dickson & product (n --> OrderedNAT) is quasi_ordered & product (n --> OrderedNAT) is antisymmetric ) ; :: thesis: verum

end;

suppose not n is zero ; :: thesis: ( not product (b₁ --> OrderedNAT) is empty & product (b₁ --> OrderedNAT) is Dickson & product (b₁ --> OrderedNAT) is quasi_ordered & product (b₁ --> OrderedNAT) is antisymmetric )

then reconsider n9 = n as non zero Element of NAT ;
reconsider p = n9 --> OrderedNAT as RelStr-yielding ManySortedSet of Segm n9 ;
thus not product (n --> OrderedNAT) is empty ; :: thesis: ( product (n --> OrderedNAT) is Dickson & product (n --> OrderedNAT) is quasi_ordered & product (n --> OrderedNAT) is antisymmetric )
for i being Element of Segm n9 holds
( p . i is Dickson & p . i is quasi_ordered ) ;
hence ( product (n --> OrderedNAT) is Dickson & product (n --> OrderedNAT) is quasi_ordered ) by Th41; :: thesis: product (n --> OrderedNAT) is antisymmetric
product p is antisymmetric ;
hence product (n --> OrderedNAT) is antisymmetric ; :: thesis: verum

end;

end;

end;

registration

let n be Element of NAT ;

cluster product (n --> OrderedNAT) -> non empty ;

coherence
not product (n --> OrderedNAT) is empty ;

cluster product (n --> OrderedNAT) -> Dickson ;

coherence
product (n --> OrderedNAT) is Dickson by Lm3;

cluster product (n --> OrderedNAT) -> quasi_ordered ;

coherence
product (n --> OrderedNAT) is quasi_ordered by Lm3;

cluster product (n --> OrderedNAT) -> antisymmetric ;

coherence
product (n --> OrderedNAT) is antisymmetric by Lm3;

end;

theorem :: DICKSON:47

for M being RelStr st M is Dickson & M is quasi_ordered holds
( [:M,OrderedNAT:] is quasi_ordered & [:M,OrderedNAT:] is Dickson ) by Th36;

:: Omitting Exercise 4.50

theorem Th47: :: DICKSON:48

for R, S being non empty RelStr st R is Dickson & S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds
S \~ is well_founded

proof end;

theorem :: DICKSON:49

for R being non empty RelStr st R is quasi_ordered holds
( R is Dickson iff for S being non empty RelStr st S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds
S \~ is well_founded )

proof end;

theorem :: DICKSON:50

NATOrd = RelIncl omega

proof end;