theorem :: PZFMISC1:27

for I being set
for x, y, A being ManySortedSet of I st {x,y} c= {A} holds
{x,y} = {A}