This is a beautiful result that clarifies a common misunderstanding of Gödel's second incompleteness theorem: the erroneous claim that a theory can only be proved consistent in a strictly stronger one. Indeed, Gentzen's theory, proving the consistency of Peano Arithmetic, is neither stronger nor weaker than PA.