Before revision: If a set of axioms is D-Complete, then any valid theorems of the system can be generated by condensed detachment alone .
After revision: If a set of axioms is D-Complete, then any valid theorem, including all of its substitution instances (up to variable renaming), of the system can be generated by condensed detachment alone .