let n be Nat; :: thesis: 3 divides Triangle ((3 * n) + 2)
a1: ((3 * n) + 2) * (n + 1) is even

proof

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

suppose n is even ; :: thesis: ((3 * n) + 2) * (n + 1) is even

hence ((3 * n) + 2) * (n + 1) is even ; :: thesis: verum

end;

suppose n is odd ; :: thesis: ((3 * n) + 2) * (n + 1) is even

hence ((3 * n) + 2) * (n + 1) is even ; :: thesis: verum

end;

end;

end;

Triangle ((3 * n) + 2) = (((3 * n) + 2) * (((3 * n) + 2) + 1)) / 2 by NUMPOLY1:19;
then Triangle ((3 * n) + 2) = 3 * ((((3 * n) + 2) * (n + 1)) / 2) ;
hence 3 divides Triangle ((3 * n) + 2) by a1; :: thesis: verum