theorem Th11: :: TAXONOM1:11

for A being non empty set holds SmallestPartition A is_finer_than {A}