:: deftheorem defines -group GROUP_10:def 17 :
for p being Nat
for G being Group holds
( G is p -group iff ex r being Nat st card G = p |^ r );