theorem Th75: :: PBOOLE:75

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