:: deftheorem Def13 defines Dickson-bases DICKSON:def 13 :
for R being non empty RelStr
for N being Subset of R st R is Dickson holds
for b₃ being non empty Subset-Family of R holds
( b₃ = Dickson-bases (N,R) iff for B being set holds
( B in b₃ iff B is_Dickson-basis_of N,R ) );