:: deftheorem defines Dickson DICKSON:def 10 :
for R being RelStr holds
( R is Dickson iff for N being Subset of R ex B being set st
( B is_Dickson-basis_of N,R & B is finite ) );