let s be SynTypes_Calculus; :: thesis: for x, y being type of s holds <*(x /" (y /" y))*> ==>. x
let x, y be type of s; :: thesis: <*(x /" (y /" y))*> ==>. x
<*x*> ==>. x by Def18;
then <*(x /" (y /" y))*> ^ H₂(s) ==>. x by Lm4, Th20;
hence <*(x /" (y /" y))*> ==>. x by FINSEQ_1:34; :: thesis: verum