let G be Group; :: thesis: for H, H1, H2 being Subgroup of G st [.H1,((Omega). G).] is Subgroup of H2 holds
[.(H1 /\ H),H.] is Subgroup of H2 /\ H
let H, H1, H2 be Subgroup of G; :: thesis: ( [.H1,((Omega). G).] is Subgroup of H2 implies [.(H1 /\ H),H.] is Subgroup of H2 /\ H )
assume A1: [.H1,((Omega). G).] is Subgroup of H2 ; :: thesis: [.(H1 /\ H),H.] is Subgroup of H2 /\ H
H1 /\ H is Subgroup of H by GROUP_2:88;
then A2: [.(H1 /\ H),H.] is Subgroup of H by Th11;
A3: H is Subgroup of (Omega). G by Lm2;
H1 /\ H is Subgroup of H1 by GROUP_2:88;
then [.(H1 /\ H),H.] is Subgroup of [.H1,((Omega). G).] by A3, GROUP_5:66;
then [.(H1 /\ H),H.] is Subgroup of H2 by A1, GROUP_2:56;
hence [.(H1 /\ H),H.] is Subgroup of H2 /\ H by A2, GROUP_2:91; :: thesis: verum