theorem :: PZFMISC1:5

for I being set
for x1, x2, X being ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff ( x = x1 or x = x2 ) ) ) holds
X = {x1,x2}