theorem Th135: :: PBOOLE:135

for I being set
for Y being ManySortedSet of I
for X being non-empty ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff x in Y ) ) holds
X = Y