Teraz wystarczy dowód korzystający z zasady substytucji przekształcić na dowód nie korzystający z tej zasady. Dowód składa się z kroków substytucji i rezolucji oraz klauzul powstałych w ich wyniku. Jeśli pewna klauzula została uzyskana w drodze substytucji, i wykorzystaliśmy ją również jedynie do substytucji, może by zastąpić tę parę jedną substytucją.
Ponieważ w końcu uzyskujemy klauzulę pustą ostatnim krokiem dowodu musi być rezolucja – substytucja nie może prowadzić do zmniejszenia liczby elementów klauzuli.
Teraz wyeliminujmy pozostałe substytucje – jedyne substytucje jakie mamy w dowodzie to substytucje klauzul, które potem będą wykorzystywane do rezolucji – ponieważ w przeciwnym wypadku ich wykluczenie nie psuje dowodu. Tak więc weźmy dowolny fragment dowodu postaci (nie muszą być one jedno po drugim w liniowej reprezentacji dowodu): przez substytucję przechodzi w rezolwuje się z dając
Ponieważ mamy przynajmniej jedną rezolucję, przynajmniej jedną substytucję (w przeciwnym wypadku dowód jest skończony), a każda substytucja jest użyta w rezolucji, zawsze będzie taki fragment.