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:20;
hence a * b = b * a ; :: thesis: verum

end;

assume a * b = b * a ; :: thesis: [.a,b.] = 1_ G
then ( (b * a) " = (b " ) * (a " ) & [.a,b.] = ((b * a) " ) * (a * b) ) by Th20, GROUP_1:26;
hence [.a,b.] = (((b " ) * (a " )) * a) * b by GROUP_1:def 4
.= (b " ) * b by GROUP_3:1
.= 1_ G by GROUP_1:def 6 ;
:: thesis: verum