theorem :: PZFMISC1:40

for I being set
for x, y, A being ManySortedSet of I holds
( {x,y} (\/) A = A iff ( x in A & y in A ) )