This DRS is true iff we can find an embedding function f, Dom(f) = {x}, which verifies all conditions in [2], which is to say that f(x) must be an A, and f verifies the complex condition [y: B(x,y)] ⇒ [z: C(x,y,z)].  The latter requirement is met iff every extension g of f, Dom(g) = {x,y}, such that g verifies [y: B(x,y)] can be extended to a function h, Dom(h) = {x,y,z}, such that h verifies [z: C(x,y,z)]. Hence, no matter how we choose g, g(x) must be the same individual as f(x), and for any g, no matter how we choose h, h(x) and h(y) must be the same as g(x) and g(y), respectively. This is why x is in the accessible domain associated with the antecedent of the conditional, and why y is in the accessible domain associated with the consequent.