theorem :: PBOOLE:47

for I being set
for X being ManySortedSet of I holds
( X (\/) (EmptyMS I) = X & (EmptyMS I) (\/) X = X ) by Th22, Th43;