theorem :: PZFMISC1:63

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|] )