theorem :: PZFMISC1:12

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