theorem :: PZFMISC1:57

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