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