let G be finite strict Group; :: thesis: ( card G > 1 implies ex a being Element of G st a <> 1_ G )
assume that
A1: card G > 1 and
A2: for a being Element of G holds a = 1_ G ; :: thesis: contradiction
for a being Element of G holds a in (1). G

proof

let a be Element of G; :: thesis: a in (1). G
a = 1_ G by A2;
then a in {(1_ G)} by TARSKI:def 1;
then a in the carrier of ((1). G) by GROUP_2:def 7;
hence a in (1). G by STRUCT_0:def 5; :: thesis: verum

end;

then multMagma(# the carrier of G,the multF of G #) = (1). G by GROUP_2:71;
hence contradiction by A1, GROUP_2:81; :: thesis: verum