  The introduction rules, also called rules of definitional closure, express reasoning ‘along’ the clauses. The elimination rule is called the principle of definitional reflection, as it reflects upon the definition as a whole. If Δ1,…, Δn exhaust all possible conditions to generate A according to the given definition, and if each of these conditions entails the very same conclusion C, then A itself entails this conclusion. If the clausal definition  is viewed as an inductive definition, this principle can be viewed as expressing the extremal clause in inductive definitions: Nothing else beyond the clauses given defines A. Obviously, definitional reflection is a generalized form of the inversion principles discussed. It develops its genuine power in definitional contexts with free variables that go beyond purely propositional reasoning, and in contexts which are not well-founded. An example of a non-wellfounded definition is the definition of an atom R by its own negation: