let i1 be Integer; :: thesis: ( i1, 0 are_congruent_mod i1 & 0 ,i1 are_congruent_mod i1 )
A1: i1 * (- 1) = 0 - i1 ;
i1 * 1 = i1 - 0 ;
hence ( i1, 0 are_congruent_mod i1 & 0 ,i1 are_congruent_mod i1 ) by A1, Def3; :: thesis: verum