let a, b, c be Integer; :: thesis: ( a divides b & a divides b + c implies a divides c )
given u being Integer such that A1: b = a * u ; :: according to INT_1:def 3 :: thesis: ( not a divides b + c or a divides c )
given t being Integer such that A2: b + c = a * t ; :: according to INT_1:def 3 :: thesis: a divides c
c = a * (t - u) by A1, A2;
hence a divides c ; :: thesis: verum