:: deftheorem Def13 defines ClOp->ClSys CLOSURE1:def 13 :
for S being 1-sorted
for A being ManySortedSet of the carrier of S
for C being MSClosureOperator of A
for b₄ being MSClosureSystem of S holds
( b₄ = ClOp->ClSys C iff ex D being MSSubsetFamily of A st
( D = MSFixPoints C & b₄ = MSClosureStr(# A,D #) ) );