theorem :: PBOOLE:49

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