theorem :: PZFMISC1:16

for I being set
for x, y being ManySortedSet of I holds
( {x} c= {x,y} & {y} c= {x,y} )