for G being Group
for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) holds
ex H being strict Subgroup of G st the carrier of H = A