for S being 1-sorted
for A being ManySortedSet of the carrier of S
for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f