let G be strict Group; :: thesis: ( G <> (1). G implies ex b being Element of G st b <> 1_ G )

assume A1: G <> (1). G ; :: thesis: ex b being Element of G st b <> 1_ G

assume A2: for b being Element of G holds not b <> 1_ G ; :: thesis: contradiction

for x, y being Element of G holds x = y

hence contradiction by A1, GROUP_6:12; :: thesis: verum

assume A1: G <> (1). G ; :: thesis: ex b being Element of G st b <> 1_ G

assume A2: for b being Element of G holds not b <> 1_ G ; :: thesis: contradiction

for x, y being Element of G holds x = y

proof end;

then
G is trivial
;hence contradiction by A1, GROUP_6:12; :: thesis: verum