theorem :: PZFMISC1:66

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