let G be strict Group; :: thesis: ( G <> (1). G implies ex b being Element of st b <> 1_ G )
assume A1: G <> (1). G ; :: thesis: ex b being Element of st b <> 1_ G
assume A2: for b being Element of holds not b <> 1_ G ; :: thesis: contradiction
for x, y being Element of holds x = y

proof

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

end;

then G is trivial by STRUCT_0:def 10;
hence contradiction by A1, GROUP_6:13; :: thesis: verum