The Causation Operator

Since C[y|F] nr> y, we have C[C[y|F]|G] < C[y|G] by left monotonicity. On the other hand, for g € IIG, g -§~> y implies g ~5~* C[y|F], which implies C[y|G] < C[C[y|F]|G], completing the demonstration.