theorem :: PBOOLE:146

for I being set
for X, Y being ManySortedSet of I st X c= Y & Y c= X holds
X = Y by Lm1;