for G being Group
for a being Element of G
for A being Subset of G st a in A holds
a in gr A