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, Def3;
A3: R is transitive by A1, Def3;
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 Th49; :: 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

assume 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, Th33;
then consider f being sequence of R such that
A5: for i, j being Element of NAT st i < j holds
not f . i <= f . j by A1, Th32;
defpred S₁[ set , set ] 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 set holds
( [x,y] in QOE iff ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) ) from RELSET_1:sch 1();
set S = RelStr(# the carrier of R,QOE #);

now

let x, y be set ; :: 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, RELAT_1:def 4;
y in rng the InternalRel of R by A7, RELAT_1:def 5;
hence [x,y] in QOE by A6, A7, A8; :: thesis: verum

end;

then A9: the InternalRel of R c= the InternalRel of RelStr(# the carrier of R,QOE #) by RELAT_1:def 3;
A10: the InternalRel of R is_reflexive_in the carrier of R by A2, ORDERS_2:def 2;

now

let x be set ; :: thesis: ( x in the carrier of R implies [x,x] in QOE )
assume A11: x in the carrier of R ; :: thesis: [x,x] in QOE
[x,x] in the InternalRel of R by A10, A11, RELAT_2:def 1;
hence [x,x] in QOE by A6, A11; :: thesis: verum

end;

then QOE is_reflexive_in the carrier of R by RELAT_2:def 1;
then A12: RelStr(# the carrier of R,QOE #) is reflexive by ORDERS_2:def 2;
A13: the InternalRel of R is_transitive_in the carrier of R by A3, ORDERS_2:def 3;

now

let x, y, z be set ; :: 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
A14: x in the carrier of R and
A15: y in the carrier of R and
A16: z in the carrier of R and
A17: [x,y] in QOE and
A18: [y,z] in QOE ; :: thesis: [x,z] in QOE

now

per 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, A17;

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

now

per 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, A18;

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

then [x,z] in the InternalRel of R by A13, A14, A15, A16, A19, RELAT_2:def 8;
hence [x,z] in QOE by A6, A14, A16; :: thesis: verum

end;

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

then consider i, j being Element of NAT such that
A20: i < j and
A21: [y,(f . j)] in the InternalRel of R and
A22: [(f . i),z] in the InternalRel of R ;
[x,(f . j)] in the InternalRel of R by A13, A14, A15, A19, A21, RELAT_2:def 8;
hence [x,z] in QOE by A6, A14, A16, A20, A22; :: thesis: verum

end;

end;

end;

hence [x,z] in QOE ; :: thesis: verum

end;

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

then consider i, j being Element of NAT such that
A23: i < j and
A24: [x,(f . j)] in the InternalRel of R and
A25: [(f . i),y] in the InternalRel of R ;

now

per 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, A18;

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

then [(f . i),z] in the InternalRel of R by A13, A15, A16, A25, RELAT_2:def 8;
hence [x,z] in QOE by A6, A14, A16, A23, A24; :: thesis: verum

end;

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

then consider a, b being Element of NAT such that
A26: a < b and
A27: [y,(f . b)] in the InternalRel of R and
A28: [(f . a),z] in the InternalRel of R ;
[(f . i),(f . b)] in the InternalRel of R by A13, A15, A25, A27, RELAT_2:def 8;
then f . i <= f . b by ORDERS_2:def 5;
then not i < b by A5;
then a <= i by A26, XXREAL_0:2;
then a < j by A23, XXREAL_0:2;
hence [x,z] in QOE by A6, A14, A16, A24, A28; :: thesis: verum

end;

end;

end;

hence [x,z] in QOE ; :: thesis: verum

end;

end;

end;

hence [x,z] in QOE ; :: thesis: verum

end;

then QOE is_transitive_in the carrier of R by RELAT_2:def 8;
then RelStr(# the carrier of R,QOE #) is transitive by ORDERS_2:def 3;
then RelStr(# the carrier of R,QOE #) is quasi_ordered by A12, Def3;
then A29: 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

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;
A30: n < n + 1 by NAT_1:13;
then not f . n1 <= f . (n1 + 1) by A5;
then A31: not [(f . n),(f . (n + 1))] in the InternalRel of R by ORDERS_2:def 5;
hence f9 . (n + 1) <> f9 . n by A10, RELAT_2:def 1; :: thesis: [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~)
A32: [(f9 . (n + 1)),(f9 . (n + 1))] in the InternalRel of R by A10, RELAT_2:def 1;
A33: [(f9 . n),(f9 . n)] in the InternalRel of R by A10, RELAT_2:def 1;

A34: now

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, A31;
then consider l, k being Element of NAT such that
A35: k < l and
A36: [(f9 . n),(f . l)] in the InternalRel of R and
A37: [(f . k),(f9 . (n + 1))] in the InternalRel of R ;
A38: f . n <= f . l by A36, ORDERS_2:def 5;
A39: f . k <= f . (n + 1) by A37, ORDERS_2:def 5;
A40: l <= n1 by A5, A38;
A41: n + 1 <= k by A5, A39;
l < n + 1 by A40, NAT_1:13;
hence contradiction by A35, A41, XXREAL_0:2; :: thesis: verum

end;

A42: [(f9 . (n1 + 1)),(f9 . n1)] in QOE by A6, A30, A32, A33;
not [(f9 . (n + 1)),(f9 . n)] in QOE ~ by A34, RELAT_1:def 7;
hence [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~) by A42, XBOOLE_0:def 5; :: thesis: verum

end;

then f9 is descending by WELLFND1:def 6;
hence contradiction by A29, WELLFND1:14; :: thesis: verum

end;

hence R is Dickson ; :: thesis: verum