let m, j be Integer; :: thesis: m * j, 0 are_congruent_mod m
take j ; :: according to INT_1:def 3 :: thesis: m * j = (m * j) - 0
thus m * j = (m * j) - 0 ; :: thesis: verum