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 ; :: 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 by A3;
consider B being set such that
A4: B is_Dickson-basis_of N',r and
A5: 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 st a in N holds
ex b being Element of st
( b in B & b <= a ) ) & B is finite )

hereby :: thesis: B is finite

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

end;

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