theorem :: PBOOLE:27

for I being set
for X, Y, Z being ManySortedSet of I holds
( X = Y (/\) Z iff ( X c= Y & X c= Z & ( for V being ManySortedSet of I st V c= Y & V c= Z holds
V c= X ) ) )