for I being set
for X, Y, Z being ManySortedSet of I st X c= Y & Y (/\) Z = EmptyMS I holds
X (/\) Z = EmptyMS I by Th44, Th19;