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