theorem Th90: :: PBOOLE:90
for I being set
for X, Y, Z being ManySortedSet of I holds (X (\+\) Y) (\+\) Z = X (\+\) (Y (\+\) Z)