theorem Th92: :: PBOOLE:92

for I being set
for X, Y being ManySortedSet of I holds X (\/) Y = X (\+\) (Y (\) X)