theorem :: GROUPP_1:28

for p being prime Nat
for G being finite strict Group st card G = p holds
G is p -commutative-group