theorem :: PZFMISC1:75

for I being set
for x, y, A, X, Y being ManySortedSet of I st A in [|x,y|] & A in [|X,Y|] holds
A in [|(x (/\) X),(y (/\) Y)|]