theorem Th1: :: MBOOLEAN:1

for I being set
for X, Y being ManySortedSet of I holds
( X = bool Y iff for A being ManySortedSet of I holds
( A in X iff A c= Y ) )