let n be non trivial Nat; :: thesis: (1 / 3) * (Triangle ((3 * n) -' 1)) = (n * ((3 * n) - 1)) / 2
A1: (3 * n) -' 1 = (3 * n) - 1 by XREAL_1:233, Th1;
Triangle ((3 * n) -' 1) = (((3 * n) - 1) * (((3 * n) - 1) + 1)) / 2 by A1, Th19;
hence (1 / 3) * (Triangle ((3 * n) -' 1)) = (n * ((3 * n) - 1)) / 2 ; :: thesis: verum