let n be Nat; :: thesis: ( n is triangular implies (9 * n) + 1 is triangular )
assume n is triangular ; :: thesis: (9 * n) + 1 is triangular
then consider k being Nat such that
A1: n = Triangle k ;
1 + (9 * (Triangle k)) = Triangle ((3 * k) + 1) by Th67;
hence (9 * n) + 1 is triangular by A1; :: thesis: verum