theorem :: PBOOLE:136

for I being set
for Y, Z 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 & x in Z ) ) ) holds
X = Y (/\) Z