theorem :: CLOSURE1:20

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