let G be Group; :: thesis: for a being Element of G
for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
let a be Element of G; :: thesis: for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
let H2 be Subgroup of G; :: thesis: ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
set A = (a * H2) * (a ");
consider x being Element of a * H2;
A1: a * H2 <> {} by Th130;
then reconsider x = x as Element of G by Lm1;

A2: now

let g be Element of G; :: thesis: ( g in (a * H2) * (a ") implies g " in (a * H2) * (a ") )
assume g in (a * H2) * (a ") ; :: thesis: g " in (a * H2) * (a ")
then consider g1 being Element of G such that
A3: g = g1 * (a ") and
A4: g1 in a * H2 by Th34;
consider g2 being Element of G such that
A5: g1 = a * g2 and
A6: g2 in H2 by A4, Th125;
g2 " in H2 by A6, Th60;
then A7: (g2 ") * (a ") in H2 * (a ") by Th126;
g " = ((a ") ") * ((a * g2) ") by A3, A5, GROUP_1:25
.= a * ((g2 ") * (a ")) by GROUP_1:25 ;
then g " in a * (H2 * (a ")) by A7, Th33;
hence g " in (a * H2) * (a ") by Th14; :: thesis: verum

end;

A8: now

let g1, g2 be Element of G; :: thesis: ( g1 in (a * H2) * (a ") & g2 in (a * H2) * (a ") implies g1 * g2 in (a * H2) * (a ") )
assume that
A9: g1 in (a * H2) * (a ") and
A10: g2 in (a * H2) * (a ") ; :: thesis: g1 * g2 in (a * H2) * (a ")
consider g being Element of G such that
A11: g1 = g * (a ") and
A12: g in a * H2 by A9, Th34;
consider h being Element of G such that
A13: g = a * h and
A14: h in H2 by A12, Th125;
(a * H2) * (a ") = a * (H2 * (a ")) by Th14;
then consider b being Element of G such that
A15: g2 = a * b and
A16: b in H2 * (a ") by A10, Th33;
consider c being Element of G such that
A17: b = c * (a ") and
A18: c in H2 by A16, Th126;
h * c in H2 by A14, A18, Th59;
then A19: a * (h * c) in a * H2 by Th125;
g1 * g2 = (a * h) * ((a ") * (a * (c * (a ")))) by A11, A15, A13, A17, GROUP_1:def 4
.= (a * h) * (((a ") * a) * (c * (a "))) by GROUP_1:def 4
.= (a * h) * ((1_ G) * (c * (a "))) by GROUP_1:def 6
.= (a * h) * (c * (a ")) by GROUP_1:def 5
.= ((a * h) * c) * (a ") by GROUP_1:def 4
.= (a * (h * c)) * (a ") by GROUP_1:def 4 ;
hence g1 * g2 in (a * H2) * (a ") by A19, Th34; :: thesis: verum

end;

x * (a ") in (a * H2) * (a ") by A1, Th34;
hence ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") by A8, A2, Th61; :: thesis: verum