let n be Nat; :: thesis: ( n is triangular implies (8 * n) + 1 is square )
assume n is triangular ; :: thesis: (8 * n) + 1 is square
then consider k being Nat such that
A1: n = Triangle k ;
(8 * (Triangle k)) + 1 = ((2 * k) + 1) ^2 by Th75;
hence (8 * n) + 1 is square by A1; :: thesis: verum