let G be Group; 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; ( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )
A1:
commutators (((1). G),H) c= {(1_ G)}
1_ G in commutators (((1). G),H)
by Th53;
hence
commutators (((1). G),H) = {(1_ G)}
by A1, ZFMISC_1:33; commutators (H,((1). G)) = {(1_ G)}
thus
commutators (H,((1). G)) c= {(1_ G)}
XBOOLE_0:def 10 {(1_ G)} c= commutators (H,((1). G))
1_ G in commutators (H,((1). G))
by Th53;
hence
{(1_ G)} c= commutators (H,((1). G))
by ZFMISC_1:31; verum