 It is because of the “or” on the right that this condition—more precisely, its ‘only if’ half—does not correspond to a sequent-to-sequent rule. Still we can ask whether some Set-Fmla proof system including the rule (∨E) (or the sequent calculus rule (∨ Left)), e.g. for classical logic, has a conservative extension to a proof system for a language with the additional connective #, whose associated consequence relation satisfies the above condition for this  #.[38]  To see that the answer to this question is negative, note that the binary relation R⊢ defined in terms of the #-supporting extension ⊢: R⊢(φ,ψ) iff φ ⊢ ψ, gives rise to a binary relational connection (L, L, R⊢) which provides conjunctive (yes—conjunctive) combinations on the left, since ⊢ is ∨-classical, φ ⋅L ψ here being φ ∨ ψ, while the inset condition above (take Γ = {χ}) secures disjunctive objects on the right, with φ +R ψ being φ # ψ. (“L” and “R” subscripts from Section  1  restored here to prevent confusion, since the source and target coincide.) Thus the crossover condition from Section  1  is satisfied, which says that if φ1 ⊢ ψ1 and φ2 ⊢ ψ2 then either φ1 ⊢ ψ2 or φ2 ⊢ ψ1. Taking φ1 = ψ1 = χ and φ2 = ψ2 = χ′, we have the antecedent of this conditional (by (Id)), so we conclude that for all formulas χ, χ′, either χ ⊢ χ′ or χ′ ⊢ χ, which includes #-free formulas of the original language (e.g., χ = p, χ′ = q) for which neither is a consequence of the other by the original consequence relation, showing any proposed extension along the above lines to be non-conservative.