Syntactic congruence universal property

For every small type $S$ of sorts, every $S$-sorted signature $\mathit{sig}$ (assigning a type of operation symbols to each finite input-sort list $w$, including $w=[]$, and output sort $s$), every $\mathit{sig}$-algebra $A$ (a carrier type $A_s$ at each sort and a total interpretation of every operation symbol), and every language $L=(L_s)_{s\in S}$ with arbitrary subsets $L_s\subseteq A_s$, let $C$ be the following syntactic congruence on $A$: a congruence means a family of equivalence relations, one on each $A_s$, preserved componentwise by every basic operation, and $x\,C_s\,y$ means that for every congruence $\Psi$ on $A$, if every congruence $\Phi$ whose classes preserve membership in $L$—that is, satisfying $\forall r\,\forall a,b\in A_r,\ a\,\Phi_r\,b\Rightarrow(a\in L_r\leftrightarrow b\in L_r)$—is pointwise contained in $\Psi$, then $x\,\Psi_s\,y$; explicitly, the containment $\Phi\leq\Psi$ means $\forall r\,\forall a,b\in A_r,\ a\,\Phi_r\,b\Rightarrow a\,\Psi_r\,b$. The theorem asserts the conjunction that $C$ itself preserves membership in $L$, namely $\forall s\,\forall x,y\in A_s,\ x\,C_s\,y\Rightarrow(x\in L_s\leftrightarrow y\in L_s)$, and that for every congruence $\Phi$ on $A$, $\Phi$ preserves membership in $L$ if and only if $\Phi\leq C$, i.e. if and only if $\forall s\,\forall x,y\in A_s,\ x\,\Phi_s\,y\Rightarrow x\,C_s\,y$. There are no assumptions that $S$, the signature, or any carrier is finite or nonempty, nor any decidable-equality assumption: $S$ may be empty (making all sortwise clauses vacuous), individual carrier sorts may be empty (making their elementwise clauses vacuous), the signature may have no symbols or may have nullary symbols where an algebra can interpret them, and $L$ may be empty, full, or otherwise arbitrary at each sort (for an empty or full component its membership-equivalence condition is automatically true).