let R be non empty RelStr ; :: thesis:
assume that
A1: R \~ is well_founded and
A2: R is connected ; :: thesis:
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:

per cases ;

suppose A3: N = {} the carrier of R ; :: thesis:

take B = {} ; :: thesis:
thus B is_Dickson-basis_of N,R by A3; :: thesis:
thus B is finite ; :: thesis:

end;

suppose A4: N <> {} the carrier of R ; :: thesis:

the InternalRel of (R \~) is_well_founded_in the carrier of (R \~) by A1, WELLFND1:def 2;
then consider b being object 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:
reconsider b = b as Element of N by A5;
thus B is_Dickson-basis_of N,R :: thesis:

proof

{b} is Subset of N by A4, SUBSET_1:33;
hence B c= N ; :: according to DICKSON:def 9 :: thesis:
let a be Element of R; :: thesis:
assume A8: a in N ; :: thesis:
reconsider b = b as Element of R by A5;
take b ; :: thesis:
thus b in B by TARSKI:def 1; :: thesis:

per cases by A2, WAYBEL_0:def 29;

suppose b <= a ; :: thesis:

hence b <= a ; :: thesis:

end;

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

then A10: [a,b] in the InternalRel of R ;

now :: thesis:

per cases ;

suppose a = b ; :: thesis:

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

end;

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

now :: thesis:

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

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

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

end;

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

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 ; :: thesis:

end;

end;

end;

hence b <= a ; :: thesis:

end;

end;

end;

hence b <= a ; :: thesis:

end;

end;

end;

thus B is finite ; :: thesis:

end;

end;