theorem :: PZFMISC1:37

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