let x, y, i, j be Integer; :: thesis: ( i,j are_relative_prime & x,y are_congruent_mod i & x,y are_congruent_mod j implies x,y are_congruent_mod i * j )
assume AS1: i,j are_relative_prime ; :: thesis: ( not x,y are_congruent_mod i or not x,y are_congruent_mod j or x,y are_congruent_mod i * j )
assume ( x,y are_congruent_mod i & x,y are_congruent_mod j ) ; :: thesis: x,y are_congruent_mod i * j
then ( i divides x - y & j divides x - y ) by INT_2:19;
then B: i lcm j divides x - y by INT_2:27;
i * j divides i lcm j by AS1, x1;
then i * j divides x - y by B, INT_2:13;
hence x,y are_congruent_mod i * j by INT_2:19; :: thesis: verum