:: deftheorem Def1 defines -power GROUPP_1:def 1 :
for p being Nat
for G being Group
for a being Element of G holds
( a is p -power iff ex r being Nat st ord a = p |^ r );