 For the following, we will take it that, as well as →, the connectives ∨, ¬, ⊤ and ⊥ are available, though in fact the result just given requires is correct for any fragment with → (with ⊢CL understood as the restriction of the classical consequence relation to the fragment in question). Then we can write the induced conditions on our consequence relation ⊢ as, respectively, rather than using a new schematic letter on the right for the first, and converting the second into conditional form: