theorem :: GROUP_1A:311

for G being addGroup
for H being Subgroup of G st G is finite holds
con_class H is finite by Th15, FINSET_1:1;