theorem :: GROUP_2:1

for G being non empty 1-sorted
for A being Subset of G st G is finite holds
A is finite ;