let G be Group; :: thesis: for H being Subgroup of G holds

( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )

let H be Subgroup of G; :: thesis: ( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )

A1: commutators (((1). G),H) c= {(1_ G)}

hence commutators (((1). G),H) = {(1_ G)} by A1, ZFMISC_1:33; :: thesis: commutators (H,((1). G)) = {(1_ G)}

thus commutators (H,((1). G)) c= {(1_ G)} :: according to XBOOLE_0:def 10 :: thesis: {(1_ G)} c= commutators (H,((1). G))

hence {(1_ G)} c= commutators (H,((1). G)) by ZFMISC_1:31; :: thesis: verum

( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )

let H be Subgroup of G; :: thesis: ( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )

A1: commutators (((1). G),H) c= {(1_ G)}

proof

1_ G in commutators (((1). G),H)
by Th53;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (((1). G),H) or x in {(1_ G)} )

assume x in commutators (((1). G),H) ; :: thesis: x in {(1_ G)}

then consider a, b being Element of G such that

A2: x = [.a,b.] and

A3: a in (1). G and

b in H by Th52;

a = 1_ G by A3, Th1;

then x = 1_ G by A2, Th19;

hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;assume x in commutators (((1). G),H) ; :: thesis: x in {(1_ G)}

then consider a, b being Element of G such that

A2: x = [.a,b.] and

A3: a in (1). G and

b in H by Th52;

a = 1_ G by A3, Th1;

then x = 1_ G by A2, Th19;

hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

hence commutators (((1). G),H) = {(1_ G)} by A1, ZFMISC_1:33; :: thesis: commutators (H,((1). G)) = {(1_ G)}

thus commutators (H,((1). G)) c= {(1_ G)} :: according to XBOOLE_0:def 10 :: thesis: {(1_ G)} c= commutators (H,((1). G))

proof

1_ G in commutators (H,((1). G))
by Th53;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators (H,((1). G)) or x in {(1_ G)} )

assume x in commutators (H,((1). G)) ; :: thesis: x in {(1_ G)}

then consider a, b being Element of G such that

A4: x = [.a,b.] and

a in H and

A5: b in (1). G by Th52;

b = 1_ G by A5, Th1;

then x = 1_ G by A4, Th19;

hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;assume x in commutators (H,((1). G)) ; :: thesis: x in {(1_ G)}

then consider a, b being Element of G such that

A4: x = [.a,b.] and

a in H and

A5: b in (1). G by Th52;

b = 1_ G by A5, Th1;

then x = 1_ G by A4, Th19;

hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

hence {(1_ G)} c= commutators (H,((1). G)) by ZFMISC_1:31; :: thesis: verum