theorem :: GROUP_3:112

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