for G being addGroup st G is finite holds
Subgroups G is finite