theorem :: PZFMISC1:71

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