theorem :: CLOSURE2:35

for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic