theorem Th7: :: GROUP_8:7

for G being Group
for a being Element of G st a <> 1_ G holds
gr {a} <> (1). G