let G be Group; :: thesis: ( G is commutative Group iff for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} )
thus ( G is commutative Group implies for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ) by Th51; :: thesis: ( ( for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ) implies G is commutative Group )
assume A1: for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ; :: thesis: G is commutative Group
G is commutative
proof
let a be Element of G; :: according to GROUP_1:def 12 :: thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * a
let b be Element of G; :: thesis: a * b = b * a
b in {b} by TARSKI:def 1;
then A2: b in gr {b} by GROUP_4:29;
a in {a} by TARSKI:def 1;
then a in gr {a} by GROUP_4:29;
then [.a,b.] in commutators ((gr {a}),(gr {b})) by A2, Th52;
then [.a,b.] in {(1_ G)} by A1;
then [.a,b.] = 1_ G by TARSKI:def 1;
hence a * b = b * a by Th36; :: thesis: verum
end;
hence G is commutative Group ; :: thesis: verum