theorem :: PBOOLE:66

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