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 & 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 A1, 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 A3: 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
A4: 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
A5: 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 A6: [x,y] in the InternalRel of R ; :: thesis: [x,y] in QOE
A7: x in dom the InternalRel of R by A6, RELAT_1:def 4;
y in rng the InternalRel of R by A6, RELAT_1:def 5;
hence [x,y] in QOE by A5, A6, A7; :: thesis: verum

end;

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

now

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

end;

then QOE is_reflexive_in the carrier of R by RELAT_2:def 1;
then A11: RelStr(# the carrier of R,QOE #) is reflexive by ORDERS_2:def 4;
A12: the InternalRel of R is_transitive_in the carrier of R by A2, ORDERS_2:def 5;

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
A13: ( x in the carrier of R & y in the carrier of R & z in the carrier of R ) and
A14: ( [x,y] in QOE & [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 A5, A14;

suppose A15: [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 A5, A14;

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

then [x,z] in the InternalRel of R by A12, A13, A15, RELAT_2:def 8;
hence [x,z] in QOE by A5, A13; :: 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
A16: ( i < j & [y,(f . j)] in the InternalRel of R & [(f . i),z] in the InternalRel of R ) ;
[x,(f . j)] in the InternalRel of R by A12, A13, A15, A16, RELAT_2:def 8;
hence [x,z] in QOE by A5, A13, A16; :: 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
A17: ( i < j & [x,(f . j)] in the InternalRel of R & [(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 A5, A14;

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

then [(f . i),z] in the InternalRel of R by A12, A13, A17, RELAT_2:def 8;
hence [x,z] in QOE by A5, A13, A17; :: 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
A18: ( a < b & [y,(f . b)] in the InternalRel of R & [(f . a),z] in the InternalRel of R ) ;
[(f . i),(f . b)] in the InternalRel of R by A12, A13, A17, A18, RELAT_2:def 8;
then f . i <= f . b by ORDERS_2:def 9;
then not i < b by A4;
then a <= i by A18, XXREAL_0:2;
then a < j by A17, XXREAL_0:2;
hence [x,z] in QOE by A5, A13, A17, A18; :: 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 5;
then RelStr(# the carrier of R,QOE #) is quasi_ordered by A11, Def3;
then A19: RelStr(# the carrier of R,QOE #) \~ is well_founded by A3, A8;
reconsider f' = f as sequence of (RelStr(# the carrier of R,QOE #) \~ ) ;

now

let n be Element of NAT ; :: thesis: ( f' . (n + 1) <> f' . n & [(f' . (n + 1)),(f' . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~ ) )
A20: n < n + 1 by NAT_1:13;
then not f . n <= f . (n + 1) by A4;
then A21: not [(f . n),(f . (n + 1))] in the InternalRel of R by ORDERS_2:def 9;
hence f' . (n + 1) <> f' . n by A9, RELAT_2:def 1; :: thesis: [(f' . (n + 1)),(f' . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~ )
A22: ( [(f' . (n + 1)),(f' . (n + 1))] in the InternalRel of R & [(f' . n),(f' . n)] in the InternalRel of R ) by A9, RELAT_2:def 1;

now

assume [(f' . n),(f' . (n + 1))] in QOE ; :: thesis: contradiction
then ex i, j being Element of NAT st
( i < j & [(f' . n),(f . j)] in the InternalRel of R & [(f . i),(f' . (n + 1))] in the InternalRel of R ) by A5, A21;
then consider l, k being Element of NAT such that
A23: k < l and
A24: ( [(f' . n),(f . l)] in the InternalRel of R & [(f . k),(f' . (n + 1))] in the InternalRel of R ) ;
( f . n <= f . l & f . k <= f . (n + 1) ) by A24, ORDERS_2:def 9;
then A25: ( l <= n & n + 1 <= k ) by A4;
then l < n + 1 by NAT_1:13;
hence contradiction by A23, A25, XXREAL_0:2; :: thesis: verum

end;

then ( [(f' . (n + 1)),(f' . n)] in QOE & not [(f' . (n + 1)),(f' . n)] in QOE ~ ) by A5, A20, A22, RELAT_1:def 7;
hence [(f' . (n + 1)),(f' . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~ ) by XBOOLE_0:def 5; :: thesis: verum

end;

then f' is descending by WELLFND1:def 7;
hence contradiction by A19, WELLFND1:15; :: thesis: verum

end;

hence R is Dickson ; :: thesis: verum