let n be Nat; :: thesis: not not n, 0 are_congruent_mod 5 & ... & not n,4 are_congruent_mod 5
not not n mod 5 = 0 & ... & not n mod 5 = 4 by Th3;
hence not not n, 0 are_congruent_mod 5 & ... & not n,4 are_congruent_mod 5 by Th4; :: thesis: verum