let n be Nat; :: thesis: (8 * (Triangle n)) + 1 = ((2 * n) + 1) ^2
8 * (Triangle n) = 8 * ((n * (n + 1)) / 2) by Th19
.= 4 * ((n ^2) + n) ;
hence (8 * (Triangle n)) + 1 = ((2 * n) + 1) ^2 ; :: thesis: verum