theorem :: NUMERAL1:9

for n being Nat holds
( 3 divides n iff 3 divides Sum (digits (n,10)) )