theorem Th36: :: CLOSURE1:36

for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for J being MSSetOp of M st ( for X being Element of bool M
for SF being non-empty MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
( J is reflexive & J is monotonic )