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

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