theorem Th7: :: CLASSES5:7

for X being non empty set holds union (SmallestPartition X) = X