:: deftheorem Def14 defines ClSys->ClOp CLOSURE1:def 14 :
for S being 1-sorted
for D being MSClosureSystem of S
for b₃ being MSClosureOperator of the Sorts of D holds
( b₃ = ClSys->ClOp D iff 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
b₃ .. X = meet SF );