theorem Th10: :: CLOSURE1:10

for I being set
for M being non-empty ManySortedSet of I
for X, Y being Element of M st X (\/) Y is Element of M holds
(id M) .. (X (\/) Y) = ((id M) .. X) (\/) ((id M) .. Y)