Nejprve ukážeme, že pro libovolné formule X a Y je {^X, X} h Y.
1. h ^X     (^y     ni) (AI)
2. {-X, X} h ^X (definice T h A pro A e T)
3. {-X, X} h -y -> -X (MP 1,2)
4. h (-y -> -nX)   (x   y) (A3)
5. {-X, X} h X     y (MP 3,4)
6. {^X, X} h X (dennice T \- A pro A e T)
7. {^X, X} h y (MP 5,6), toto jsme chtěli ukázat, dále podle věty o dedukci
8. {-X} h X    y (VD7)
9. h ^X —> (X —> y) (VD8), nyní můžeme uvážit speciální případ volby X — ~^A, Y — -^^^A, který už jsme mohli dosazovat od začátku, ale takhle jsme si ukázali navíc obecnější pravidlo, že ze sporných předpokladů je možné dokázat cokoli.
10. {^A} h ^A —>• -.-.-.A (dosazení do 8)
11. h [pA — —A)     (-.-.A -> A) (A3)
12. {—A} h -h-iA     A (MP 10,11)
13. {—.4} h ^ (VD12)
14. h ^A -> A (VD13)
1