let R be non empty RelStr ; :: thesis: ( R is quasi_ordered implies ( 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 ) )

assume A1: R is quasi_ordered ; :: thesis: ( 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 )

A2: R is reflexive by A1;

A3: R is transitive by A1;

set IR = the InternalRel of R;

set CR = the carrier of R;

thus ( R is Dickson implies 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 ) by Th47; :: thesis: ( ( 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 ) implies R is Dickson )

assume A4: 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 ; :: thesis: R is Dickson

S \~ is well_founded ) )

assume A1: R is quasi_ordered ; :: thesis: ( 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 )

A2: R is reflexive by A1;

A3: R is transitive by A1;

set IR = the InternalRel of R;

set CR = the carrier of R;

thus ( R is Dickson implies 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 ) by Th47; :: thesis: ( ( 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 ) implies R is Dickson )

assume A4: 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 ; :: thesis: R is Dickson

now :: thesis: R is Dickson

hence
R is Dickson
; :: thesis: verumassume
not R is Dickson
; :: thesis: contradiction

then not for N being non empty Subset of R holds

( min-classes N is finite & not min-classes N is empty ) by A1, Th31;

then consider f being sequence of R such that

A5: for i, j being Nat st i < j holds

not f . i <= f . j by A1, Th30;

defpred S_{1}[ object , object ] means ( [$1,$2] in the InternalRel of R or ex i, j being Element of NAT st

( i < j & [$1,(f . j)] in the InternalRel of R & [(f . i),$2] in the InternalRel of R ) );

consider QOE being Relation of the carrier of R, the carrier of R such that

A6: for x, y being object holds

( [x,y] in QOE iff ( x in the carrier of R & y in the carrier of R & S_{1}[x,y] ) )
from RELSET_1:sch 1();

set S = RelStr(# the carrier of R,QOE #);

A10: the InternalRel of R is_reflexive_in the carrier of R by A2;

then for x being object st x in the carrier of R holds

[x,x] in QOE by A6;

then QOE is_reflexive_in the carrier of R ;

then A11: RelStr(# the carrier of R,QOE #) is reflexive ;

A12: the InternalRel of R is_transitive_in the carrier of R by A3;

then RelStr(# the carrier of R,QOE #) is transitive ;

then RelStr(# the carrier of R,QOE #) is quasi_ordered by A11;

then A28: RelStr(# the carrier of R,QOE #) \~ is well_founded by A4, A9;

reconsider f9 = f as sequence of (RelStr(# the carrier of R,QOE #) \~) ;

hence contradiction by A28, WELLFND1:14; :: thesis: verum

end;then not for N being non empty Subset of R holds

( min-classes N is finite & not min-classes N is empty ) by A1, Th31;

then consider f being sequence of R such that

A5: for i, j being Nat st i < j holds

not f . i <= f . j by A1, Th30;

defpred S

( i < j & [$1,(f . j)] in the InternalRel of R & [(f . i),$2] in the InternalRel of R ) );

consider QOE being Relation of the carrier of R, the carrier of R such that

A6: for x, y being object holds

( [x,y] in QOE iff ( x in the carrier of R & y in the carrier of R & S

set S = RelStr(# the carrier of R,QOE #);

now :: thesis: for x, y being object st [x,y] in the InternalRel of R holds

[x,y] in QOE

then A9:
the InternalRel of R c= the InternalRel of RelStr(# the carrier of R,QOE #)
by RELAT_1:def 3;[x,y] in QOE

let x, y be object ; :: thesis: ( [x,y] in the InternalRel of R implies [x,y] in QOE )

assume A7: [x,y] in the InternalRel of R ; :: thesis: [x,y] in QOE

A8: x in dom the InternalRel of R by A7, XTUPLE_0:def 12;

y in rng the InternalRel of R by A7, XTUPLE_0:def 13;

hence [x,y] in QOE by A6, A7, A8; :: thesis: verum

end;assume A7: [x,y] in the InternalRel of R ; :: thesis: [x,y] in QOE

A8: x in dom the InternalRel of R by A7, XTUPLE_0:def 12;

y in rng the InternalRel of R by A7, XTUPLE_0:def 13;

hence [x,y] in QOE by A6, A7, A8; :: thesis: verum

A10: the InternalRel of R is_reflexive_in the carrier of R by A2;

then for x being object st x in the carrier of R holds

[x,x] in QOE by A6;

then QOE is_reflexive_in the carrier of R ;

then A11: RelStr(# the carrier of R,QOE #) is reflexive ;

A12: the InternalRel of R is_transitive_in the carrier of R by A3;

now :: thesis: for x, y, z being object st x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in QOE & [y,z] in QOE holds

[x,z] in QOE

then
QOE is_transitive_in the carrier of R
;[x,z] in QOE

let x, y, z be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in QOE & [y,z] in QOE implies [x,z] in QOE )

assume that

A13: x in the carrier of R and

A14: y in the carrier of R and

A15: z in the carrier of R and

A16: [x,y] in QOE and

A17: [y,z] in QOE ; :: thesis: [x,z] in QOE

end;assume that

A13: x in the carrier of R and

A14: y in the carrier of R and

A15: z in the carrier of R and

A16: [x,y] in QOE and

A17: [y,z] in QOE ; :: thesis: [x,z] in QOE

now :: thesis: [x,z] in QOEend;

hence
[x,z] in QOE
; :: thesis: verumper cases
( [x,y] in the InternalRel of R or ex i, j being Element of NAT st

( i < j & [x,(f . j)] in the InternalRel of R & [(f . i),y] in the InternalRel of R ) ) by A6, A16;

end;

( i < j & [x,(f . j)] in the InternalRel of R & [(f . i),y] in the InternalRel of R ) ) by A6, A16;

suppose A18:
[x,y] in the InternalRel of R
; :: thesis: [x,z] in QOE

end;

now :: thesis: [x,z] in QOEend;

hence
[x,z] in QOE
; :: thesis: verumper cases
( [y,z] in the InternalRel of R or ex i, j being Element of NAT st

( i < j & [y,(f . j)] in the InternalRel of R & [(f . i),z] in the InternalRel of R ) ) by A6, A17;

end;

( i < j & [y,(f . j)] in the InternalRel of R & [(f . i),z] in the InternalRel of R ) ) by A6, A17;

suppose
[y,z] in the InternalRel of R
; :: thesis: [x,z] in QOE

then
[x,z] in the InternalRel of R
by A12, A13, A14, A15, A18;

hence [x,z] in QOE by A6, A13, A15; :: thesis: verum

end;hence [x,z] in QOE by A6, A13, A15; :: thesis: verum

suppose
ex i, j being Element of NAT st

( i < j & [y,(f . j)] in the InternalRel of R & [(f . i),z] in the InternalRel of R ) ; :: thesis: [x,z] in QOE

( i < j & [y,(f . j)] in the InternalRel of R & [(f . i),z] in the InternalRel of R ) ; :: thesis: [x,z] in QOE

then consider i, j being Element of NAT such that

A19: i < j and

A20: [y,(f . j)] in the InternalRel of R and

A21: [(f . i),z] in the InternalRel of R ;

[x,(f . j)] in the InternalRel of R by A12, A13, A14, A18, A20;

hence [x,z] in QOE by A6, A13, A15, A19, A21; :: thesis: verum

end;A19: i < j and

A20: [y,(f . j)] in the InternalRel of R and

A21: [(f . i),z] in the InternalRel of R ;

[x,(f . j)] in the InternalRel of R by A12, A13, A14, A18, A20;

hence [x,z] in QOE by A6, A13, A15, A19, A21; :: thesis: verum

suppose
ex i, j being Element of NAT st

( i < j & [x,(f . j)] in the InternalRel of R & [(f . i),y] in the InternalRel of R ) ; :: thesis: [x,z] in QOE

( i < j & [x,(f . j)] in the InternalRel of R & [(f . i),y] in the InternalRel of R ) ; :: thesis: [x,z] in QOE

then consider i, j being Element of NAT such that

A22: i < j and

A23: [x,(f . j)] in the InternalRel of R and

A24: [(f . i),y] in the InternalRel of R ;

end;A22: i < j and

A23: [x,(f . j)] in the InternalRel of R and

A24: [(f . i),y] in the InternalRel of R ;

now :: thesis: [x,z] in QOEend;

hence
[x,z] in QOE
; :: thesis: verumper cases
( [y,z] in the InternalRel of R or ex a, b being Element of NAT st

( a < b & [y,(f . b)] in the InternalRel of R & [(f . a),z] in the InternalRel of R ) ) by A6, A17;

end;

( a < b & [y,(f . b)] in the InternalRel of R & [(f . a),z] in the InternalRel of R ) ) by A6, A17;

suppose
[y,z] in the InternalRel of R
; :: thesis: [x,z] in QOE

then
[(f . i),z] in the InternalRel of R
by A12, A14, A15, A24;

hence [x,z] in QOE by A6, A13, A15, A22, A23; :: thesis: verum

end;hence [x,z] in QOE by A6, A13, A15, A22, A23; :: thesis: verum

suppose
ex a, b being Element of NAT st

( a < b & [y,(f . b)] in the InternalRel of R & [(f . a),z] in the InternalRel of R ) ; :: thesis: [x,z] in QOE

( a < b & [y,(f . b)] in the InternalRel of R & [(f . a),z] in the InternalRel of R ) ; :: thesis: [x,z] in QOE

then consider a, b being Element of NAT such that

A25: a < b and

A26: [y,(f . b)] in the InternalRel of R and

A27: [(f . a),z] in the InternalRel of R ;

[(f . i),(f . b)] in the InternalRel of R by A12, A14, A24, A26;

then f . i <= f . b ;

then not i < b by A5;

then a <= i by A25, XXREAL_0:2;

then a < j by A22, XXREAL_0:2;

hence [x,z] in QOE by A6, A13, A15, A23, A27; :: thesis: verum

end;A25: a < b and

A26: [y,(f . b)] in the InternalRel of R and

A27: [(f . a),z] in the InternalRel of R ;

[(f . i),(f . b)] in the InternalRel of R by A12, A14, A24, A26;

then f . i <= f . b ;

then not i < b by A5;

then a <= i by A25, XXREAL_0:2;

then a < j by A22, XXREAL_0:2;

hence [x,z] in QOE by A6, A13, A15, A23, A27; :: thesis: verum

then RelStr(# the carrier of R,QOE #) is transitive ;

then RelStr(# the carrier of R,QOE #) is quasi_ordered by A11;

then A28: RelStr(# the carrier of R,QOE #) \~ is well_founded by A4, A9;

reconsider f9 = f as sequence of (RelStr(# the carrier of R,QOE #) \~) ;

now :: thesis: for n being Nat holds

( f9 . (n + 1) <> f9 . n & [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~) )

then
f9 is descending
by WELLFND1:def 6;( f9 . (n + 1) <> f9 . n & [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~) )

let n be Nat; :: thesis: ( f9 . (n + 1) <> f9 . n & [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~) )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A29: n < n + 1 by NAT_1:13;

then not f . n1 <= f . (n1 + 1) by A5;

then A30: not [(f . n),(f . (n + 1))] in the InternalRel of R ;

hence f9 . (n + 1) <> f9 . n by A10; :: thesis: [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~)

A31: [(f9 . (n + 1)),(f9 . (n + 1))] in the InternalRel of R by A10;

A32: [(f9 . n),(f9 . n)] in the InternalRel of R by A10;

not [(f9 . (n + 1)),(f9 . n)] in QOE ~ by A33, RELAT_1:def 7;

hence [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~) by A41, XBOOLE_0:def 5; :: thesis: verum

end;reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A29: n < n + 1 by NAT_1:13;

then not f . n1 <= f . (n1 + 1) by A5;

then A30: not [(f . n),(f . (n + 1))] in the InternalRel of R ;

hence f9 . (n + 1) <> f9 . n by A10; :: thesis: [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~)

A31: [(f9 . (n + 1)),(f9 . (n + 1))] in the InternalRel of R by A10;

A32: [(f9 . n),(f9 . n)] in the InternalRel of R by A10;

A33: now :: thesis: not [(f9 . n),(f9 . (n + 1))] in QOE

A41:
[(f9 . (n1 + 1)),(f9 . n1)] in QOE
by A6, A29, A31, A32;assume
[(f9 . n),(f9 . (n + 1))] in QOE
; :: thesis: contradiction

then ex i, j being Element of NAT st

( i < j & [(f9 . n),(f . j)] in the InternalRel of R & [(f . i),(f9 . (n + 1))] in the InternalRel of R ) by A6, A30;

then consider l, k being Element of NAT such that

A34: k < l and

A35: [(f9 . n),(f . l)] in the InternalRel of R and

A36: [(f . k),(f9 . (n + 1))] in the InternalRel of R ;

A37: f . n <= f . l by A35;

A38: f . k <= f . (n + 1) by A36;

A39: l <= n1 by A5, A37;

A40: n + 1 <= k by A5, A38;

l < n + 1 by A39, NAT_1:13;

hence contradiction by A34, A40, XXREAL_0:2; :: thesis: verum

end;then ex i, j being Element of NAT st

( i < j & [(f9 . n),(f . j)] in the InternalRel of R & [(f . i),(f9 . (n + 1))] in the InternalRel of R ) by A6, A30;

then consider l, k being Element of NAT such that

A34: k < l and

A35: [(f9 . n),(f . l)] in the InternalRel of R and

A36: [(f . k),(f9 . (n + 1))] in the InternalRel of R ;

A37: f . n <= f . l by A35;

A38: f . k <= f . (n + 1) by A36;

A39: l <= n1 by A5, A37;

A40: n + 1 <= k by A5, A38;

l < n + 1 by A39, NAT_1:13;

hence contradiction by A34, A40, XXREAL_0:2; :: thesis: verum

not [(f9 . (n + 1)),(f9 . n)] in QOE ~ by A33, RELAT_1:def 7;

hence [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~) by A41, XBOOLE_0:def 5; :: thesis: verum

hence contradiction by A28, WELLFND1:14; :: thesis: verum