theorem Th11: :: GROUP_8:11

for G being strict Group
for b being Element of G st not b is being_of_order_0 holds
gr {b} is finite