= Disjunction property of regular theories
{title2=$\mathbb T\vdash\phi\Rightarrow\bigvee_i\psi_i\ \Longrightarrow\ \exists i\ \mathbb T\vdash\phi\Rightarrow\psi_i$}
If a regular theory proves an outer coherent sequent $\phi\vdash\bigvee_{i=1}^n\psi_i$ with all formulas regular, it proves $\phi\vdash\psi_i$ for some $i$. In the classifying topos, the corresponding subobjects cover the representable associated with $\phi$. Irreducibility of that representable and full faithfulness of the syntactic Yoneda embedding produce the desired derivation.
Back to article page
