theorem :: NUMBER02:38

for n being Nat holds
( not 10 divides n iff ex k being Nat st
( n = (10 * k) + 1 or n = (10 * k) + 2 or n = (10 * k) + 3 or n = (10 * k) + 4 or n = (10 * k) + 5 or n = (10 * k) + 6 or n = (10 * k) + 7 or n = (10 * k) + 8 or n = (10 * k) + 9 ) )