theorem :: PZFMISC1:67

for I being set
for A, B, X, Y being ManySortedSet of I st A c= X & B c= Y holds
[|A,Y|] (/\) [|X,B|] = [|A,B|]