theorem :: PZFMISC1:69

for I being set
for x1, x2, A, B being ManySortedSet of I holds [|x1,x2|] (\) [|A,B|] = [|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|]