theorem Th94: :: PBOOLE:94

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