:: deftheorem Def23 defines ClSys->ClOp CLOSURE2:def 23 :
for S being 1-sorted
for D being ClosureSystem of S
for b₃ being ClosureOperator of the Sorts of D holds
( b₃ = ClSys->ClOp D iff for x being Element of Bool the Sorts of D holds b₃ . x = Cl x );