theorem Th104: :: CARD_3:107

for I being set
for f being non-empty ManySortedSet of I
for s being b₂ -compatible ManySortedSet of I holds s in product f