:: deftheorem Def2 defines expon GROUPP_1:def 2 :
for p being prime Nat
for G being Group st G is p -group holds
for b₃ being Nat holds
( b₃ = expon (G,p) iff card G = p |^ b₃ );