let n be triangular number ; :: thesis: not n,9 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,9 are_congruent_mod 10 ; :: thesis: contradiction
then ((k * (k + 1)) / 2) * 2,9 * 2 are_congruent_mod 10 * 2 by A3, INT_4:10;
then k * (k + 1),18 are_congruent_mod 5 by A2, INT_1:20;
then 18,k * (k + 1) are_congruent_mod 5 by INT_1:14;
then 18 - 5,k * (k + 1) are_congruent_mod 5 by INT_1:22;
then 13 - 5,k * (k + 1) are_congruent_mod 5 by INT_1:22;
then 8 - 5,k * (k + 1) are_congruent_mod 5 by INT_1:22;
then 3,(k * k) + k are_congruent_mod 5 ;
hence contradiction by Th7, INT_1:14; :: thesis: verum