theorem :: PRE_CIRC:2

for I being set
for MSS being ManySortedSet of I holds (MSS #) . (<*> I) = {{}}