theorem :: CLASSES5:8

for X being non empty set holds X, SmallestPartition X are_equipotent