theorem :: CLOSURE1:40

for S being 1-sorted
for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)