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