:: deftheorem PerPowDef defines perfect_power NUMBER06:def 10 :
for n being Nat holds
( n is perfect_power iff ex x, k being Nat st
( k > 1 & n = x |^ k ) );