theorem :: GROUPP_1:28
for p being Prime
for G being finite strict Group st card G = p holds
G is p -commutative-group