let G be Group; :: thesis: for a, b being Element of G holds
( [.a,b.] = 1_ G iff a * b = b * a )
let a, b be Element of G; :: thesis: ( [.a,b.] = 1_ G iff a * b = b * a )
thus ( [.a,b.] = 1_ G implies a * b = b * a ) :: thesis: ( a * b = b * a implies [.a,b.] = 1_ G )

proof

assume [.a,b.] = 1_ G ; :: thesis: a * b = b * a
then ((b * a) ") * (a * b) = 1_ G by Th20;
then a * b = ((b * a) ") " by GROUP_1:12;
hence a * b = b * a ; :: thesis: verum

end;

assume a * b = b * a ; :: thesis: [.a,b.] = 1_ G
then A1: (b * a) " = (b ") * (a ") by GROUP_1:18;
[.a,b.] = ((b * a) ") * (a * b) by Th20;
hence [.a,b.] = (((b ") * (a ")) * a) * b by A1, GROUP_1:def 3
.= (b ") * b by GROUP_3:1
.= 1_ G by GROUP_1:def 5 ;
:: thesis: verum