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)} )
thus commutators ((1). G),H = {(1_ G)} :: thesis: commutators H,((1). G) = {(1_ G)}

proof

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

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
A1: ( x = [.a,b.] & a in (1). G & b in H ) by Th58;
a = 1_ G by A1, Th1;
then x = 1_ G by A1, Th22;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

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

end;

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
A2: ( x = [.a,b.] & a in H & b in (1). G ) by Th58;
b = 1_ G by A2, Th1;
then x = 1_ G by A2, 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