theorem :: PZFMISC1:68

for I being set
for X, Y, Z being ManySortedSet of I holds
( [|(X (\) Y),Z|] = [|X,Z|] (\) [|Y,Z|] & [|Z,(X (\) Y)|] = [|Z,X|] (\) [|Z,Y|] )