theorem Th70: :: PBOOLE:70

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