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 N9 = N as Subset of r by A3;
consider B being set such that
A4: B is_Dickson-basis_of N9,r and
A5: B is finite by A2;
take B ; :: thesis: ( B is_Dickson-basis_of N,s & B is finite )
thus B c= N by A4; :: 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 b9 being Element of s st
( b9 in B & b9 <= a ) )
assume A6: a in N ; :: thesis: ex b9 being Element of s st
( b9 in B & b9 <= a )
reconsider a9 = a as Element of r by A3;
consider b being Element of r such that
A7: b in B and
A8: b <= a9 by A4, A6;
reconsider b9 = b as Element of s by A3;
take b9 = b9; :: thesis: ( b9 in B & b9 <= a )
[b,a9] in the InternalRel of r by A8;
hence ( b9 in B & b9 <= a ) by A1, A7; :: thesis: verum
end;
thus B is finite by A5; :: thesis: verum