theorem :: GROUP_3:101

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