theorem Th6: :: NAT_6:6

for p being Prime
for a being Integer holds
( a gcd p <> 1 iff p divides a )