theorem Th73: :: PBOOLE:73

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