let n be Nat; :: thesis: not not n, 0 are_congruent_mod 10 & ... & not n,9 are_congruent_mod 10
not not n mod 10 = 0 & ... & not n mod 10 = 9 by Th8;
hence not not n, 0 are_congruent_mod 10 & ... & not n,9 are_congruent_mod 10 by Th4; :: thesis: verum