let n be Nat; :: thesis: not not n mod 5 = 0 & ... & not n mod 5 = 4
n mod 5 < 4 + 1 by NAT_D:1;
then n mod 5 <= 4 by NAT_1:13;
hence not not n mod 5 = 0 & ... & not n mod 5 = 4 ; :: thesis: verum