for n being Nat
for p being prime Nat 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 )