theorem :: PZFMISC1:71

for I being set
for x, X being ManySortedSet of I st X is non-empty holds
( [|{x},X|] is non-empty & [|X,{x}|] is non-empty )