theorem :: CLOSURE1:38

for S being 1-sorted
for D being MSClosureSystem of S
for J being MSSetOp of the Sorts of D st ( for X being Element of bool the Sorts of D
for SF being non-empty MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is MSClosureOperator of the Sorts of D by Th36, Th37;