theorem Th16: :: GROUPP_1:16

for G being Group
for p being prime Nat holds (1). G is p -group