let G be Group; :: thesis: for a, b being Element of G holds

( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )

let a, b be Element of G; :: thesis: ( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )

thus [.a,b,(1_ G).] = 1_ G by Th19; :: thesis: ( [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )

thus [.a,(1_ G),b.] = [.(1_ G),b.] by Th19

.= 1_ G by Th19 ; :: thesis: [.(1_ G),a,b.] = 1_ G

thus [.(1_ G),a,b.] = [.(1_ G),b.] by Th19

.= 1_ G by Th19 ; :: thesis: verum

( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )

let a, b be Element of G; :: thesis: ( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )

thus [.a,b,(1_ G).] = 1_ G by Th19; :: thesis: ( [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )

thus [.a,(1_ G),b.] = [.(1_ G),b.] by Th19

.= 1_ G by Th19 ; :: thesis: [.(1_ G),a,b.] = 1_ G

thus [.(1_ G),a,b.] = [.(1_ G),b.] by Th19

.= 1_ G by Th19 ; :: thesis: verum