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;
hence a in (1). G by GROUP_2:def 7; :: thesis: verum

end;

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