for I being set
for Y, Z being ManySortedSet of I
for X being V8() ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff ( x in Y & x in Z ) ) ) holds
X = Y (/\) Z