theorem Th23: :: PBOOLE:23

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