theorem :: CLOSURE2:31

for I being set
for M being ManySortedSet of I
for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent