theorem Th15: :: PBOOLE:15

for I being set
for X, Y being ManySortedSet of I holds X (/\) Y c= X