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)}

proof

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;

1_ G in commutators (((1). G),H) by Th53;
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

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;

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