let G be strict Group; :: thesis: ( G is commutative Group iff G ` = (1). G )
thus ( G is commutative Group implies G ` = (1). G ) :: thesis: ( G ` = (1). G implies G is commutative Group )

proof

assume A1: G is commutative Group ; :: thesis: G ` = (1). G

now :: thesis: for a being Element of G st a in G ` holds
a in (1). G

let a be Element of G; :: thesis: ( a in G ` implies a in (1). G )
assume a in G ` ; :: thesis: a in (1). G
then a in gr {(1_ G)} by A1, Th51;
then a in gr ({(1_ G)} \ {(1_ G)}) by GROUP_4:35;
then a in gr ({} the carrier of G) by XBOOLE_1:37;
hence a in (1). G by GROUP_4:30; :: thesis: verum

end;

then A2: G ` is Subgroup of (1). G by GROUP_2:58;
(1). G is Subgroup of G ` by GROUP_2:65;
hence G ` = (1). G by A2, GROUP_2:55; :: thesis: verum

end;

assume A3: G ` = (1). G ; :: thesis: G is commutative Group
G is commutative

proof

let a, b be Element of G; :: according to GROUP_1:def 12 :: thesis: a * b = b * a
[.a,b.] in G ` by Th74;
then [.a,b.] = 1_ G by A3, Th1;
hence a * b = b * a by Th36; :: thesis: verum

end;

hence G is commutative Group ; :: thesis: verum