let r, s be RelStr ; :: thesis: ( the InternalRel of r c= the InternalRel of s & r is Dickson & the carrier of r = the carrier of s implies s is Dickson )
assume that
A1: the InternalRel of r c= the InternalRel of s and
A2: r is Dickson and
A3: the carrier of r = the carrier of s ; :: thesis: s is Dickson
let N be Subset of s; :: according to DICKSON:def 10 :: thesis: ex B being set st
( B is_Dickson-basis_of N,s & B is finite )
reconsider N' = N as Subset of r by A3;
consider B being set such that
A4: ( B is_Dickson-basis_of N',r & B is finite ) by A2, Def10;
take B ; :: thesis: ( B is_Dickson-basis_of N,s & B is finite )
thus B c= N by A4, Def9; :: according to DICKSON:def 9 :: thesis: ( ( for a being Element of s st a in N holds
ex b being Element of s st
( b in B & b <= a ) ) & B is finite )

hereby :: thesis: B is finite

let a be Element of s; :: thesis: ( a in N implies ex b' being Element of s st
( b' in B & b' <= a ) )
assume A5: a in N ; :: thesis: ex b' being Element of s st
( b' in B & b' <= a )
reconsider a' = a as Element of r by A3;
consider b being Element of r such that
A6: ( b in B & b <= a' ) by A4, A5, Def9;
reconsider b' = b as Element of s by A3;
take b' = b'; :: thesis: ( b' in B & b' <= a )
[b,a'] in the InternalRel of r by A6, ORDERS_2:def 9;
hence ( b' in B & b' <= a ) by A1, A6, ORDERS_2:def 9; :: thesis: verum

end;

thus B is finite by A4; :: thesis: verum