let G be Group; :: thesis: for a, b being Element of G holds [.a,a,b.] = 1_ G
let a, b be Element of G; :: thesis: [.a,a,b.] = 1_ G
thus [.a,a,b.] = [.(1_ G),b.] by Th23
.= 1_ G by Th22 ; :: thesis: verum