let t, u, z be Integer; :: thesis: ( u divides t + z & u divides t - z implies ( u divides 2 * t & u divides 2 * z ) )
A0: ( t + z = (t + t) + (z - t) & t + z = (t - z) + (z + z) ) ;
assume A1: ( u divides t + z & u divides t - z ) ; :: thesis: ( u divides 2 * t & u divides 2 * z )
then u divides - (t - z) by INT_2:10;
hence ( u divides 2 * t & u divides 2 * z ) by A0, A1, INT_2:1; :: thesis: verum