theorem Th11: :: GR_CY_1:11
for G being finite strict Group st card G > 1 holds
ex a being Element of G st a <> 1_ G