theorem Th15: :: GROUP_1A:216

for G being addGroup st G is finite holds
Subgroups G is finite