let x be set ; for G being Group holds
( x in commutators G iff ex a, b being Element of G st x = [.a,b.] )
let G be Group; ( x in commutators G iff ex a, b being Element of G st x = [.a,b.] )
thus
( x in commutators G implies ex a, b being Element of G st x = [.a,b.] )
( ex a, b being Element of G st x = [.a,b.] implies x in commutators G )
given a, b being Element of G such that A1:
x = [.a,b.]
; x in commutators G
thus
x in commutators G
by A1; verum