Disjunction property of regular theories ($\mathbb{T}⊢\varphi \Rightarrow {\bigvee }_i{\psi }_i⟹\exists i\mathbb{T}⊢\varphi \Rightarrow {\psi }_i$)

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.