theorem Th52: :: PBOOLE:52

for I being set
for X, Y being ManySortedSet of I holds
( X (\) Y = EmptyMS I iff X c= Y )