In this paper we prove that any subexpression of a correct judgement in Martin-Löf's Type Theory is strongly normalizable. We use the well-established technique with a ``computability predicate''. The logic used in the proof is classical set theory.