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