theorem Th68: :: GROUP_1A:114

for G being addGroup holds (0). G is finite