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

begin

theorem Th1: :: DICKSON:1

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

proof end;

theorem Th2: :: DICKSON:2

for n being Nat holds n c= n + 1

proof end;

scheme :: DICKSON:sch 1
FinSegRng2{ F₁() -> Element of NAT , F₂() -> Element of NAT , F₃( set ) -> set , P₁[ set ] } :

{ F₃(i) where i is Element of NAT : ( F₁() < i & i <= F₂() & P₁[i] ) } is finite

proof end;

theorem Th3: :: DICKSON:3

for X being infinite set ex f being Function of NAT,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 :Def2: :: DICKSON:def 2
for n being Element of NAT holds [(f . n),(f . (n + 1))] in the InternalRel of R;

end;

:: deftheorem Def2 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 Element of NAT holds [(f . n),(f . (n + 1))] in the InternalRel of R );

theorem Th4: :: 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 Element of NAT st i < j holds
f . i <= f . j

proof end;

theorem Th5: :: 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 :: DICKSON:6

canceled;

theorem Th7: :: DICKSON:7

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 Th8: :: DICKSON:8

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;

begin

definition

let R be RelStr ;
attr R is quasi_ordered means :Def3: :: DICKSON:def 3
( R is reflexive & R is transitive );

end;

:: deftheorem Def3 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 Th9: :: DICKSON:9

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 set 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 set 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 set 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 set 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 set 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 Th10: :: DICKSON:10

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

proof end;

theorem :: DICKSON:11

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:12

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

proof end;

theorem :: DICKSON:13

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

proof end;

theorem :: DICKSON:14

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

proof end;

theorem :: DICKSON:15

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 Th16: :: DICKSON:16

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

proof end;

theorem Th17: :: DICKSON:17

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

proof end;

begin

theorem Th18: :: DICKSON:18

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;

theorem :: DICKSON:19

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 Th20: :: DICKSON:20

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 Th21: :: DICKSON:21

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

proof end;

theorem Th22: :: DICKSON:22

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 Th23: :: DICKSON:23

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 Th24: :: DICKSON:24

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:25

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 :Def9: :: 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 Def9 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 Th26: :: DICKSON:26

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

proof end;

theorem Th27: :: DICKSON:27

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 :Def10: :: 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 Def10 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 Th28: :: DICKSON:28

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

proof end;

theorem Th29: :: DICKSON:29

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 Th30: :: DICKSON:30

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

proof end;

theorem Th31: :: DICKSON:31

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 Th32: :: DICKSON:32

for R being non empty RelStr st R is quasi_ordered & ( for f being sequence of R ex i, j being Element of 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 Th33: :: DICKSON:33

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 Th34: :: DICKSON:34

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

proof end;

theorem :: DICKSON:35

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 Th36: :: DICKSON:36

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 Th37: :: DICKSON:37

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

proof end;

theorem Th38: :: DICKSON:38

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 Th39: :: DICKSON:39

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 Th40: :: DICKSON:40

for p being RelStr-yielding ManySortedSet of 1
for z being Element of 1 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 Th41: :: DICKSON:41

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

proof end;

theorem Th42: :: DICKSON:42

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

proof end;

theorem Th43: :: DICKSON:43

for n being non empty Nat
for p being RelStr-yielding ManySortedSet of n st ( for i being Element of 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

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 Th44: :: DICKSON:44

NATOrd is_reflexive_in NAT

proof end;

theorem Th45: :: DICKSON:45

NATOrd is_antisymmetric_in NAT

proof end;

theorem Th46: :: DICKSON:46

NATOrd is_strongly_connected_in NAT

proof end;

theorem Th47: :: DICKSON:47

NATOrd is_transitive_in NAT

proof end;

definition

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

end;

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

Lm2: now

now

let x, y be Element of OrderedNAT; :: thesis: ( not x <= y implies y <= x )
assume not x <= y ; :: thesis: y <= x
then not [x,y] in NATOrd by ORDERS_2:def 9;
then [y,x] in NATOrd by Th46, RELAT_2:def 7;
hence y <= x by ORDERS_2:def 9; :: thesis: verum

end;

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 Th45, ORDERS_2:def 6;
cluster OrderedNAT -> non empty transitive ;
coherence
OrderedNAT is transitive by Th47, ORDERS_2:def 5;
cluster OrderedNAT -> non empty well_founded ;
coherence
OrderedNAT is well_founded

proof end;

end;

Lm3: now

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 empty or not n is empty ) ;

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

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 empty ; :: 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 empty Element of NAT ;
set p = n9 --> OrderedNAT;
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 n9 holds
( (n9 --> OrderedNAT) . i is Dickson & (n9 --> OrderedNAT) . i is quasi_ordered ) by FUNCOP_1:13;
hence ( product (n --> OrderedNAT) is Dickson & product (n --> OrderedNAT) is quasi_ordered ) by Th43; :: thesis: product (n --> OrderedNAT) is antisymmetric
product (n9 --> OrderedNAT) 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:48

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

theorem Th49: :: DICKSON:49

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:50

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;