let x be set ; :: thesis: for G being Group
for H1, H2 being Subgroup of G holds
( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )

let G be Group; :: thesis: for H1, H2 being Subgroup of G holds
( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )

let H1, H2 be Subgroup of G; :: thesis: ( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )

thus ( x in commutators (H1,H2) implies ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) ) :: thesis: ( ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) implies x in commutators (H1,H2) )
proof
assume x in commutators (H1,H2) ; :: thesis: ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 )

then consider a, b being Element of G such that
A1: x = [.a,b.] and
A2: ( a in carr H1 & b in carr H2 ) ;
( a in H1 & b in H2 ) by ;
hence ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) by A1; :: thesis: verum
end;
given a, b being Element of G such that A3: x = [.a,b.] and
A4: ( a in H1 & b in H2 ) ; :: thesis: x in commutators (H1,H2)
( a in carr H1 & b in carr H2 ) by ;
hence x in commutators (H1,H2) by A3; :: thesis: verum