 Disjunction property of regular theories

If a regular theory proves an outer coherent sequent $\varphi ⊢{\bigvee }_{i=1}^n{\psi }_i$ with all formulas regular, it proves $\varphi ⊢{\psi }_i$ for some $i$. In the classifying topos, the corresponding subobjects cover the representable associated with $\varphi$. Irreducibility of that representable and full faithfulness of the syntactic Yoneda embedding produce the desired derivation.