let t, u be Integer; :: thesis: ( t is even & t,u are_coprime implies u is odd )
A1: (2 * 0) + 1 is odd ;
assume ( t is even & t,u are_coprime & not u is odd ) ; :: thesis: contradiction
hence contradiction by A1, Th9; :: thesis: verum