theorem :: PZFMISC1:78

for I being set
for X, Y being ManySortedSet of I st X (/\) Y = EmptyMS I holds
[|X,Y|] (/\) [|Y,X|] = EmptyMS I