:: deftheorem Def2 defines Strong_Classification TAXONOM1:def 2 :
for A being non empty set
for b₂ being Subset of (PARTITIONS A) holds
( b₂ is Strong_Classification of A iff ( b₂ is Classification of A & {A} in b₂ & SmallestPartition A in b₂ ) );