take F = I --> (id c); :: thesis: cods F = I --> c
cods F = I --> (cod (id c)) by Th5;
hence cods F = I --> c ; :: thesis: verum