let R be non empty RelStr ; :: thesis: ( R is quasi_ordered & ( for N being non empty Subset of holds
( min-classes N is finite & not min-classes N is empty ) ) implies R is Dickson )
assume that
A1: R is quasi_ordered and
A2: for N being non empty Subset of holds
( min-classes N is finite & not min-classes N is empty ) ; :: thesis: R is Dickson
A3: R is transitive by A1, Def3;
A4: R is reflexive by A1, Def3;
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR' = the InternalRel of (R \~ );
let N be Subset of ; :: according to DICKSON:def 10 :: thesis: ex B being set st
( B is_Dickson-basis_of N,R & B is finite )

per cases ( N = {} the carrier of R or not N is empty ) ;

suppose A5: N = {} the carrier of R ; :: thesis: ex B being set st
( B is_Dickson-basis_of N,R & B is finite )

take B = {} ; :: thesis: ( B is_Dickson-basis_of N,R & B is finite )
thus B is_Dickson-basis_of N,R by A5, Th26; :: thesis: B is finite
thus B is finite ; :: thesis: verum

end;

suppose not N is empty ; :: thesis: ex B being set st
( B is_Dickson-basis_of N,R & B is finite )

then reconsider N' = N as non empty Subset of ;
reconsider MCN' = min-classes N' as non empty finite Subset-Family of by A2;
take B = { (choose x) where x is Element of MCN' : verum } ; :: thesis: ( B is_Dickson-basis_of N,R & B is finite )
thus B is_Dickson-basis_of N,R :: thesis: B is finite

proof

now

let x be set ; :: thesis: ( x in B implies x in N )
assume x in B ; :: thesis: x in N
then consider y being Element of MCN' such that
A6: x = choose y ;
A7: ex z being Element of st
( z is_minimal_wrt N,the InternalRel of (R \~ ) & y = (Class (EqRel R),z) /\ N ) by Def8;
not y is empty by Th23;
hence x in N by A6, A7, XBOOLE_0:def 4; :: thesis: verum

end;

hence B c= N by TARSKI:def 3; :: according to DICKSON:def 9 :: thesis: for a being Element of st a in N holds
ex b being Element of st
( b in B & b <= a )
let a be Element of ; :: thesis: ( a in N implies ex b being Element of st
( b in B & b <= a ) )
assume A8: a in N ; :: thesis: ex b being Element of st
( b in B & b <= a )
defpred S₁[ Element of ] means $1 <= a;
set NN' = { d where d is Element of N' : S₁[d] } ;
A9: { d where d is Element of N' : S₁[d] } is Subset of from DOMAIN_1:sch 7();
a <= a by A4, ORDERS_2:24;
then a in { d where d is Element of N' : S₁[d] } by A8;
then reconsider NN' = { d where d is Element of N' : S₁[d] } as non empty Subset of by A9, XBOOLE_1:1;
consider m being Element of min-classes NN';
A10: not min-classes NN' is empty by A2;
then reconsider m' = m as non empty set by Th23;
consider c being Element of m';
consider y being Element of such that
y is_minimal_wrt NN',the InternalRel of (R \~ ) and
A11: m' = (Class (EqRel R),y) /\ NN' by A10, Def8;
A12: c in Class (EqRel R),y by A11, XBOOLE_0:def 4;
A13: c in NN' by A11, XBOOLE_0:def 4;
reconsider c = c as Element of by A12;
reconsider c' = c as Element of ;
A14: ex d being Element of N' st
( c = d & d <= a ) by A13;
A15: c is_minimal_wrt NN',the InternalRel of (R \~ ) by A1, A10, Th20;

now

assume not c is_minimal_wrt N,the InternalRel of (R \~ ) ; :: thesis: contradiction
then consider w being set such that
A16: w in N and
A17: w <> c and
A18: [w,c] in the InternalRel of (R \~ ) by A14, WAYBEL_4:def 26;
reconsider w' = w as Element of by A18, ZFMISC_1:106;
w' <= c' by A18, ORDERS_2:def 9;
then w' <= a by A3, A14, ORDERS_2:26;
then w' in NN' by A16;
hence contradiction by A15, A17, A18, WAYBEL_4:def 26; :: thesis: verum

end;

then A19: (Class (EqRel R),c) /\ N in min-classes N by Def8;
then A20: not (Class (EqRel R),c) /\ N is empty by Th23;
set t = choose ((Class (EqRel R),c) /\ N);
choose ((Class (EqRel R),c) /\ N) in N by A20, XBOOLE_0:def 4;
then reconsider t = choose ((Class (EqRel R),c) /\ N) as Element of ;
take t ; :: thesis: ( t in B & t <= a )
thus t in B by A19; :: thesis: t <= a
t in Class (EqRel R),c by A20, XBOOLE_0:def 4;
then [t,c] in EqRel R by EQREL_1:27;
then [t,c] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
then [t,c] in the InternalRel of R by XBOOLE_0:def 4;
then t <= c' by ORDERS_2:def 9;
hence t <= a by A3, A14, ORDERS_2:26; :: thesis: verum

end;

deffunc H₁( set ) -> Element of $1 = choose $1;
defpred S₁[ set ] means verum;
{ H₁(x) where x is Element of MCN' : S₁[x] } is finite from PRE_CIRC:sch 1();
hence B is finite ; :: thesis: verum

end;

end;