:: deftheorem Def1 defines Classification TAXONOM1:def 1 :
for A being non empty set
for b₂ being Subset of (PARTITIONS A) holds
( b₂ is Classification of A iff for X, Y being a_partition of A st X in b₂ & Y in b₂ & not X is_finer_than Y holds
Y is_finer_than X );