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
G is trivial

proof

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

proof

let x, y be Element of G; :: thesis: x = y
x = 1_ G by A2;
hence x = y by A2; :: thesis: verum

end;

hence G is trivial by STRUCT_0:def 10; :: thesis: verum

end;

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