for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds ((FNegation I) * (FNegation I)) * (FNegation I) = FNegation I