for I being set
for M being V8() V39() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds
B c= A ) holds
ex m being ManySortedSet of I st
( m in M & ( for K being ManySortedSet of I st K in M holds
K c= m ) )