theorem :: GROUP_1A:300

for G being addGroup
for A being Subset of G st G is finite holds
con_class A is finite ;