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 set ; :: 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 Th58;
a = 1_ G by A3, Th1;
then x = 1_ G by A2, Th22;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

1_ G in commutators ((1). G),H by Th59;
hence commutators ((1). G),H = {(1_ G)} by A1, ZFMISC_1:39; :: 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 set ; :: 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 Th58;
b = 1_ G by A5, Th1;
then x = 1_ G by A4, Th22;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

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