let t, u, z be Integer; :: thesis: ( t,z are_coprime & t,u are_coprime & t is even implies ( u + z is even & u - z is even & u * z is odd ) )
assume ( t,z are_coprime & t,u are_coprime & t is even ) ; :: thesis: ( u + z is even & u - z is even & u * z is odd )
then ( z is odd & u is odd ) by Lm20;
hence ( u + z is even & u - z is even & u * z is odd ) ; :: thesis: verum