theorem Th104: :: CARD_3:107

for I being set
for f being V8() ManySortedSet of I
for s being b₂ -compatible ManySortedSet of I holds s in product f