theorem :: CLOSURE1:21

for I being set
for M being ManySortedSet of I
for P, R being MSSetOp of M st P is monotonic & R is monotonic holds
P ** R is monotonic