theorem :: MBOOLEAN:18

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