let R be non empty RelStr ; :: thesis: ( R \~ is well_founded & R is connected implies R is Dickson )
assume that
A1: R \~ is well_founded and
A2: R is connected ; :: thesis: R is Dickson
set IR9 = the InternalRel of (R \~ );
set CR9 = the carrier of (R \~ );
set IR = the InternalRel of R;
set CR = the carrier 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 N <> {} the carrier of R ) ;

suppose A3: 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 A3, Th26; :: thesis: B is finite
thus B is finite ; :: thesis: verum

end;

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

the InternalRel of (R \~ ) is_well_founded_in the carrier of (R \~ ) by A1, WELLFND1:def 2;
then consider b being set such that
A5: b in N and
A6: the InternalRel of (R \~ ) -Seg b misses N by A4, WELLORD1:def 3;
A7: (the InternalRel of (R \~ ) -Seg b) /\ N = {} by A6, XBOOLE_0:def 7;
take B = {b}; :: thesis: ( B is_Dickson-basis_of N,R & B is finite )
reconsider b = b as Element of N by A5;
thus B is_Dickson-basis_of N,R :: thesis: B is finite

proof

{b} is Subset of N by A4, SUBSET_1:55;
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 )
reconsider b = b as Element of R by A5;
take b ; :: thesis: ( b in B & b <= a )
thus b in B by TARSKI:def 1; :: thesis: b <= a

per cases ( b <= a or a <= b ) by A2, WAYBEL_0:def 29;

suppose b <= a ; :: thesis: b <= a

hence b <= a ; :: thesis: verum

end;

suppose A9: a <= b ; :: thesis: b <= a

then A10: [a,b] in the InternalRel of R by ORDERS_2:def 9;

now

per cases ( a = b or not a = b ) ;

suppose a = b ; :: thesis: b <= a

hence b <= a by A9; :: thesis: verum

end;

suppose A11: not a = b ; :: thesis: b <= a

now

per cases ( [a,b] in the InternalRel of (R \~ ) or not [a,b] in the InternalRel of (R \~ ) ) ;

suppose [a,b] in the InternalRel of (R \~ ) ; :: thesis: b <= a

then a in the InternalRel of (R \~ ) -Seg b by A11, WELLORD1:def 1;
hence b <= a by A7, A8, XBOOLE_0:def 4; :: thesis: verum

end;

suppose not [a,b] in the InternalRel of (R \~ ) ; :: thesis: b <= a

then [a,b] in the InternalRel of R ~ by A10, XBOOLE_0:def 5;
then [b,a] in the InternalRel of R by RELAT_1:def 7;
hence b <= a by ORDERS_2:def 9; :: thesis: verum

end;

end;

end;

hence b <= a ; :: thesis: verum

end;

end;

end;

hence b <= a ; :: thesis: verum

end;

end;

end;

thus B is finite ; :: thesis: verum

end;

end;