:: deftheorem defines -commutative-group GROUPP_1:def 4 :
for p being Nat
for G being Group holds
( G is p -commutative-group iff ( G is p -group & G is p -commutative-group-like ) );