theorem Th12: :: TOPGEN_2:12

for X being set holds card (SmallestPartition X) = card X