let x be Integer; :: thesis: 2 divides x * (x + 1)

per cases ( x is even or x is odd ) ;

suppose x is even ; :: thesis: 2 divides x * (x + 1)

hence 2 divides x * (x + 1) by ABIAN:def 1; :: thesis: verum

end;

suppose x is odd ; :: thesis: 2 divides x * (x + 1)

then consider y being Integer such that
A1: x = (2 * y) + 1 by ABIAN:1;
x * (x + 1) = 2 * (((2 * y) + 1) * (y + 1)) by A1;
hence 2 divides x * (x + 1) by INT_1:def 3; :: thesis: verum

end;

end;