theorem Th46: :: NUMBER02:46

for a being Nat st not 7 divides a holds
ex k being Nat st
( a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 )