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;