let G be Group; :: thesis: for A1 being Subset of G st A1 = { [.a,b.] where a, b is Element of G : verum } holds
G ` = gr A1
let A1 be Subset of G; :: thesis: ( A1 = { [.a,b.] where a, b is Element of G : verum } implies G ` = gr A1 )
assume A1: A1 = { [.a,b.] where a, b is Element of G : verum } ; :: thesis: G ` = gr A1
A1 = commutators G

proof

thus A1 c= commutators G :: according to XBOOLE_0:def 10 :: thesis: commutators G c= A1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A1 or x in commutators G )
assume x in A1 ; :: thesis: x in commutators G
then ex a, b being Element of G st x = [.a,b.] by A1;
hence x in commutators G by GROUP_5:58; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in commutators G or x in A1 )
assume x in commutators G ; :: thesis: x in A1
then ex a, b being Element of G st x = [.a,b.] by GROUP_5:58;
hence x in A1 by A1; :: thesis: verum

end;

hence G ` = gr A1 by GROUP_5:72; :: thesis: verum