let G be Group; :: thesis: for a being Element of G holds [.a,a.] = 1_ G
let a be Element of G; :: thesis: [.a,a.] = 1_ G
thus [.a,a.] = ((a * a) ") * (a * a) by Th17
.= 1_ G by GROUP_1:def 5 ; :: thesis: verum