let s be SynTypes_Calculus; :: thesis: for x being type of s holds x <==>. x
let x be type of s; :: thesis: x <==>. x
<*x*> ==>. x by Def19;
hence x <==>. x by Def20; :: thesis: verum