In the following we define what it takes for an embedding function to verify a DRS or DRS-condition in a given model. As usual, a model M is a pair &lt;D,I&gt;, where D is a set of individuals, and I is an interpretation function that assigns sets of individuals to one-place predicates, sets of pairs to two-place predicates, and so on. To enhance the legibility of our definition somewhat we omit the qualifier “in M” throughout: