theorem Th7: :: GR_CY_1:7

for G being finite Group
for a being Element of G holds ord a = card (gr {a})