I've been reading this extremely important principle recently and I couldn't help noticing that a proof of this principle is somehow "missing" in the two books I'm reading: (the advanced one) Categories for Working Mathematicians by Lane and (the easy one) Abstract and Concrete Categories by Adamek. I do understand that such a principle's proof is natural and trivial, but I still wonder if there is a more rigorous way to state the prove it.
(1) I've read the proof of this principle for both boolean algebras and preorders, but I couldn't find any proof of this principle for all categories. Stated in Abstract and Concrete Categories,
"[...] Every statement $\mathcal S_{\mathbf A^\text{op}}(X)$ concerning an object $X$ in the category $\mathbf A^{\text{op}}$ can be translated into a logically equivalent statement $\mathcal S^{\text{op}}_\mathcal A (X)$ concerning the object $X$ in the category $\mathbf A$."
Intuitively, this must be true, but is there a rigorous way of proving it? The duality principle implies that for all categories, property $$\mathcal P\text{ holds}\iff \mathcal{P}^{\text{op}}\text{ holds}.$$ I can prove this theorem: since $\mathcal P$ holds for all categories, $\mathcal P(C)\implies\mathcal P(C^{\text{op}})\implies\mathcal{P}^{\text{op}}(C)$ and since $(C^{\text{op}})^{\text{op}}=C$, the converse suffices. But all of these are based on a rigorous proof of the quoted statement. Can anyone tell me how to prove the quotation rigorously?
(2) Also, is the version of the duality principle above the same as $$\text{ETAC}\vdash \Sigma\implies \text{ETAC}\vdash \Sigma^{*}?$$ where ETAC is the elementary theory of an abstract category.