theorem Th23: :: GROUP_8:23

for G being strict Group st G <> (1). G holds
ex b being Element of G st b <> 1_ G