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;