theorem Th7: :: PBOOLE:7

for I being set
for x, X, Y being ManySortedSet of I st ( x in X or x in Y ) holds
x in X (\/) Y