theorem :: CLOSURE2:42

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