 The second clause of the theorem below, in this particular instance, says that the formula \(A\) above is derivable in first-order logic if and only if there are sequences of variables \(x_{2}^1, x_{4}^1, \ldots, x_2^n, x_4 ^n\) and terms \(s_{1}^1, s_{3}^1, \ldots, s_1^n,  s_3 ^n\) in the original language such that \[ B(s_{1}^1, x_{2}^1, s_{3}^1, x_4 ^1 ) \vee \ldots \vee B(s_1^n, x_2^n, s_3^n, x_4^n ) \] is a quasi-tautology, and such that \(A\) is derivable from   this formula using only the quantifier and idempotency rules described below.