let G be Group; :: thesis: for a, b being Element of G

for H1, H2 being Subgroup of G st a in H1 & b in H2 holds

[.a,b.] in [.H1,H2.]

let a, b be Element of G; :: thesis: for H1, H2 being Subgroup of G st a in H1 & b in H2 holds

[.a,b.] in [.H1,H2.]

let H1, H2 be Subgroup of G; :: thesis: ( a in H1 & b in H2 implies [.a,b.] in [.H1,H2.] )

assume ( a in H1 & b in H2 ) ; :: thesis: [.a,b.] in [.H1,H2.]

then ( a in carr H1 & b in carr H2 ) by STRUCT_0:def 5;

hence [.a,b.] in [.H1,H2.] by Th60; :: thesis: verum

for H1, H2 being Subgroup of G st a in H1 & b in H2 holds

[.a,b.] in [.H1,H2.]

let a, b be Element of G; :: thesis: for H1, H2 being Subgroup of G st a in H1 & b in H2 holds

[.a,b.] in [.H1,H2.]

let H1, H2 be Subgroup of G; :: thesis: ( a in H1 & b in H2 implies [.a,b.] in [.H1,H2.] )

assume ( a in H1 & b in H2 ) ; :: thesis: [.a,b.] in [.H1,H2.]

then ( a in carr H1 & b in carr H2 ) by STRUCT_0:def 5;

hence [.a,b.] in [.H1,H2.] by Th60; :: thesis: verum