:: deftheorem defines solves_CRT NUMBER14:def 1 :
for a1, n1, a2, n2, x being Integer holds
( x solves_CRT a1,n1,a2,n2 iff ( x,a1 are_congruent_mod n1 & x,a2 are_congruent_mod n2 ) );