let R be non empty RelStr ; :: thesis: ( R is quasi_ordered & ( for N being non empty Subset of R 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 R holds
( min-classes N is finite & not min-classes N is empty ) ; :: thesis: R is Dickson
A3: R is transitive by A1;
A4: R is reflexive by A1;
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);
let N be Subset of the carrier of R; :: 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; :: 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 N9 = N as non empty Subset of the carrier of R ;
reconsider MCN9 = min-classes N9 as non empty finite Subset-Family of the carrier of R by A2;
take B = { the Element of x where x is Element of MCN9 : 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 :: thesis: for x being object st x in B holds
x in N

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

end;

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

now :: thesis: c is_minimal_wrt N, the InternalRel of (R \~)

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 25;
reconsider w9 = w as Element of R by A18, ZFMISC_1:87;
w9 <= c9 by A18;
then w9 <= a by A3, A14, ORDERS_2:3;
then w9 in NN9 by A16;
hence contradiction by A15, A17, A18, WAYBEL_4:def 25; :: 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 Th21;
set t = the Element of (Class ((EqRel R),c)) /\ N;
the Element of (Class ((EqRel R),c)) /\ N in N by A20, XBOOLE_0:def 4;
then reconsider t = the Element of (Class ((EqRel R),c)) /\ N as Element of R ;
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:19;
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 <= c9 ;
hence t <= a by A3, A14, ORDERS_2:3; :: thesis: verum

end;

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

end;

end;