let n be triangular number ; :: thesis: not n,2 are_congruent_mod 10
consider k being Nat such that
A1: n = Triangle k by Def2;
A2: 4 * 5 = 20 ;
A3: n = (k * (k + 1)) / 2 by A1, Th19;
assume n,2 are_congruent_mod 10 ; :: thesis: contradiction
then ((k * (k + 1)) / 2) * 2,2 * 2 are_congruent_mod 10 * 2 by A3, INT_4:10;
then k * (k + 1),4 are_congruent_mod 5 by A2, INT_1:20;
then 4,(k * k) + k are_congruent_mod 5 by INT_1:14;
hence contradiction by Th6, INT_1:14; :: thesis: verum