theorem :: PZFMISC1:72

for I being set
for x, y, X being ManySortedSet of I holds
( [|{x,y},X|] = [|{x},X|] (\/) [|{y},X|] & [|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|] )