theorem Th14: :: YELLOW20:14

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