:: deftheorem Def21 defines ClOp->ClSys CLOSURE2:def 21 :
for S being 1-sorted
for A being ManySortedSet of the carrier of S
for g being ClosureOperator of A
for b₄ being strict ClosureStr over S holds
( b₄ = ClOp->ClSys g iff ( the Sorts of b₄ = A & the Family of b₄ = { x where x is Element of Bool A : g . x = x } ) );