let x be set ; :: thesis: 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; :: thesis: ( 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.] ) :: thesis: ( ex a, b being Element of G st x = [.a,b.] implies x in commutators G )

thus x in commutators G by A1; :: thesis: verum

( x in commutators G iff ex a, b being Element of G st x = [.a,b.] )

let G be Group; :: thesis: ( 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.] ) :: thesis: ( ex a, b being Element of G st x = [.a,b.] implies x in commutators G )

proof

given a, b being Element of G such that A1:
x = [.a,b.]
; :: thesis: x in commutators G
assume
x in commutators G
; :: thesis: ex a, b being Element of G st x = [.a,b.]

then ex a, b being Element of G st

( x = [.a,b.] & a in (Omega). G & b in (Omega). G ) by Th52;

hence ex a, b being Element of G st x = [.a,b.] ; :: thesis: verum

end;then ex a, b being Element of G st

( x = [.a,b.] & a in (Omega). G & b in (Omega). G ) by Th52;

hence ex a, b being Element of G st x = [.a,b.] ; :: thesis: verum

thus x in commutators G by A1; :: thesis: verum