for X being set
for p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q}