for I being non empty set
for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X (/\) Y <> EmptyMS I by Th8, Th124;