let n be Nat; :: thesis: (3 * (Triangle n)) + (Triangle (n + 1)) = Triangle ((2 * n) + 1)
A1: Triangle n = (n * (n + 1)) / 2 by Th19;
A2: Triangle (n + 1) = ((n + 1) * ((n + 1) + 1)) / 2 by Th19
.= ((n + 1) * (n + 2)) / 2 ;
Triangle ((2 * n) + 1) = (((2 * n) + 1) * (((2 * n) + 1) + 1)) / 2 by Th19
.= (((2 * n) + 1) * ((2 * n) + 2)) / 2 ;
hence (3 * (Triangle n)) + (Triangle (n + 1)) = Triangle ((2 * n) + 1) by A1, A2; :: thesis: verum