 This theorem can be expressed and proved in PRA and ensures that a T-proof of a “real”, finitistically meaningful statement A leads to a finitistically valid statement. This point is made clear in Hilbert’s 1927-Hamburg lecture (Hilbert 1927). There he takes A to be the Fermat proposition and argues that if we had a proof of A in a theory containing “ideal” elements, a finistist consistency proof for that theory would allow us to transform that proof into a finitist one.