let X be non empty set ; :: thesis: X, SmallestPartition X are_equipotent
card X = card (SmallestPartition X) by TOPGEN_2:12;
hence X, SmallestPartition X are_equipotent by CARD_1:5; :: thesis: verum