for t, u, z being Integer st u divides t + z & u divides t - z holds
( u divides 2 * t & u divides 2 * z )