theorem Th13: :: GROUP_8:13

for G being strict Group
for b being Element of G holds
( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds
n = 0 )