theorem Th14: :: PBOOLE:14

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