 Let us give a sketch of the proof of Löb’s theorem itself from his derivability conditions (the proof of the formalized version is similar). The proof is based on Gödel’s diagonalization lemma, which says that for any arithmetical formula \(C(x)\) there is an arithmetical formula \(B\) such that