let G be Group; 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; ( [.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; ( [.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
; [.(1_ G),a,b.] = 1_ G
thus [.(1_ G),a,b.] =
[.(1_ G),b.]
by Th19
.=
1_ G
by Th19
; verum