let s be SynTypes_Calculus; :: thesis: for x, y being type of s holds x /" y <==>. x /" ((x /" y) \ x)
let x, y be type of s; :: thesis: x /" y <==>. x /" ((x /" y) \ x)
A1: <*(x /" y)*> ==>. x /" ((x /" y) \ x) by Th13;
<*(x /" ((x /" y) \ x))*> ==>. x /" y by Th18;
hence x /" y <==>. x /" ((x /" y) \ x) by A1, Def20; :: thesis: verum