:: deftheorem defines [= PBOOLE:def 11 :
for I being set
for X, Y being ManySortedSet of I holds
( X [= Y iff for x being ManySortedSet of I st x in X holds
x in Y );