theorem :: PZFMISC1:42

for I being set
for x, y, X being ManySortedSet of I st not I is empty holds
{x,y} (\/) X <> EmptyMS I