:: deftheorem Def6 defines distribution_family DIST_1:def 6 :
for S being finite set
for b₂ being Subset-Family of (S *) holds
( b₂ = distribution_family S iff for A being Subset of (S *) holds
( A in b₂ iff ex s being FinSequence of S st A = Finseq-EQclass s ) );