theorem Th15: :: OSALG_2:15

for I being set
for M being ManySortedSet of I
for x being set holds
( x is ManySortedSubset of M iff x in product (bool M) )