:: deftheorem defines is_Dickson-basis_of DICKSON:def 9 :
for R being RelStr
for N being Subset of R
for B being set holds
( B is_Dickson-basis_of N,R iff ( B c= N & ( for a being Element of R st a in N holds
ex b being Element of R st
( b in B & b <= a ) ) ) );