theorem Th1: :: GROUPP_1:1

for n being Nat
for p being Prime st ( for r being Nat holds n <> p |^ r ) holds
ex s being Element of NAT st
( s is prime & s divides n & s <> p )