for I being set
for X, Y, Z being ManySortedSet of I st X (\) Y c= Z & Y (\) X c= Z holds
X (\+\) Y c= Z by Th16;