theorem :: PBOOLE:24

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