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 )

proof

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;

given a, b being Element of G such that A1: x = [.a,b.] ; :: thesis: x in commutators G
thus x in commutators G by A1; :: thesis: verum