theorem Th95: :: PBOOLE:95

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