theorem :: YELLOW20:13

for I being set
for A, B being ManySortedSet of I holds Intersect (A,B) = A (/\) B