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 Th20
.= 1_ G by GROUP_1:def 6 ; :: thesis: verum