for i1 being Integer holds
( i1, 0 are_congruent_mod i1 & 0 ,i1 are_congruent_mod i1 )