Очевидно, что С' — действительно базовый экземпляр выражения С. Вообще говоря, для того чтобы выражения С1' и С2' имели какие-либо резольвенты, они должны быть получены путем предварительного применения к выражениям С1 и С2 наиболее общего унификатора для пары взаимно дополнительных литералов в C1 и С2. Из леммы поднятия можно легко получить аналогичное, приведенное ниже утверждение о любой последовательности применений правила резолюции.

Для любого выражения С в резолюционном замыкании множества выражений S' существует выражение С в резолюционном замыкании множества выражений S, такое, что С — базовый экземпляр выражения с и логический вывод с имеет такую же длину, как и логический вывод с'.

Из этого факта следует, что если в резолюционном замыкании множества выражений S' появляется пустое выражение, оно должно также появиться в резолюционном замыкании множества выражений s. Это связано с тем, что пустое выражение не может быть базовым экземпляром любого другого выражения. Подведем итог: мы показали, что если множество выражений S невыполнимо, то для него существует конечная процедура логического вывода пустого выражения с помощью правила резолюции.

Поднятие способа доказательства теорем от базовых выражений к выражениям первого порядка обеспечивает огромное увеличение мощи доказательства. Это увеличение связано с тем фактом, что теперь в доказательстве первого порядка конкретизация переменных может выполняться только по мере того, как это потребуется для самого доказательства, тогда как в методах с использованием базовых выражений приходилось исследовать огромное количество произвольных конкретизации.