theorem Th68: :: PBOOLE:68

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