set A = (carr H1) /\ (carr H2);

1_ G in H2 by Lm17;

then A1: 1_ G in the carrier of H2 by STRUCT_0:def 5;

then 1_ G in the carrier of H1 by STRUCT_0:def 5;

then (carr H1) /\ (carr H2) <> {} by A1, XBOOLE_0:def 4;

hence ex b_{1} being strict StableSubgroup of G st the carrier of b_{1} = (carr H1) /\ (carr H2)
by A2, A11, A8, Lm14; :: thesis: verum

1_ G in H2 by Lm17;

then A1: 1_ G in the carrier of H2 by STRUCT_0:def 5;

A2: now :: thesis: for g1, g2 being Element of G st g1 in (carr H1) /\ (carr H2) & g2 in (carr H1) /\ (carr H2) holds

g1 * g2 in (carr H1) /\ (carr H2)

g1 * g2 in (carr H1) /\ (carr H2)

let g1, g2 be Element of G; :: thesis: ( g1 in (carr H1) /\ (carr H2) & g2 in (carr H1) /\ (carr H2) implies g1 * g2 in (carr H1) /\ (carr H2) )

assume that

A3: g1 in (carr H1) /\ (carr H2) and

A4: g2 in (carr H1) /\ (carr H2) ; :: thesis: g1 * g2 in (carr H1) /\ (carr H2)

g2 in carr H2 by A4, XBOOLE_0:def 4;

then A5: g2 in H2 by STRUCT_0:def 5;

g1 in carr H2 by A3, XBOOLE_0:def 4;

then g1 in H2 by STRUCT_0:def 5;

then g1 * g2 in H2 by A5, Lm18;

then A6: g1 * g2 in carr H2 by STRUCT_0:def 5;

g2 in carr H1 by A4, XBOOLE_0:def 4;

then A7: g2 in H1 by STRUCT_0:def 5;

g1 in carr H1 by A3, XBOOLE_0:def 4;

then g1 in H1 by STRUCT_0:def 5;

then g1 * g2 in H1 by A7, Lm18;

then g1 * g2 in carr H1 by STRUCT_0:def 5;

hence g1 * g2 in (carr H1) /\ (carr H2) by A6, XBOOLE_0:def 4; :: thesis: verum

end;assume that

A3: g1 in (carr H1) /\ (carr H2) and

A4: g2 in (carr H1) /\ (carr H2) ; :: thesis: g1 * g2 in (carr H1) /\ (carr H2)

g2 in carr H2 by A4, XBOOLE_0:def 4;

then A5: g2 in H2 by STRUCT_0:def 5;

g1 in carr H2 by A3, XBOOLE_0:def 4;

then g1 in H2 by STRUCT_0:def 5;

then g1 * g2 in H2 by A5, Lm18;

then A6: g1 * g2 in carr H2 by STRUCT_0:def 5;

g2 in carr H1 by A4, XBOOLE_0:def 4;

then A7: g2 in H1 by STRUCT_0:def 5;

g1 in carr H1 by A3, XBOOLE_0:def 4;

then g1 in H1 by STRUCT_0:def 5;

then g1 * g2 in H1 by A7, Lm18;

then g1 * g2 in carr H1 by STRUCT_0:def 5;

hence g1 * g2 in (carr H1) /\ (carr H2) by A6, XBOOLE_0:def 4; :: thesis: verum

A8: now :: thesis: for o being Element of O

for a being Element of G st a in (carr H1) /\ (carr H2) holds

(G ^ o) . a in (carr H1) /\ (carr H2)

for a being Element of G st a in (carr H1) /\ (carr H2) holds

(G ^ o) . a in (carr H1) /\ (carr H2)

let o be Element of O; :: thesis: for a being Element of G st a in (carr H1) /\ (carr H2) holds

(G ^ o) . a in (carr H1) /\ (carr H2)

let a be Element of G; :: thesis: ( a in (carr H1) /\ (carr H2) implies (G ^ o) . a in (carr H1) /\ (carr H2) )

assume A9: a in (carr H1) /\ (carr H2) ; :: thesis: (G ^ o) . a in (carr H1) /\ (carr H2)

then a in carr H2 by XBOOLE_0:def 4;

then a in H2 by STRUCT_0:def 5;

then (G ^ o) . a in H2 by Lm9;

then A10: (G ^ o) . a in carr H2 by STRUCT_0:def 5;

a in carr H1 by A9, XBOOLE_0:def 4;

then a in H1 by STRUCT_0:def 5;

then (G ^ o) . a in H1 by Lm9;

then (G ^ o) . a in carr H1 by STRUCT_0:def 5;

hence (G ^ o) . a in (carr H1) /\ (carr H2) by A10, XBOOLE_0:def 4; :: thesis: verum

end;(G ^ o) . a in (carr H1) /\ (carr H2)

let a be Element of G; :: thesis: ( a in (carr H1) /\ (carr H2) implies (G ^ o) . a in (carr H1) /\ (carr H2) )

assume A9: a in (carr H1) /\ (carr H2) ; :: thesis: (G ^ o) . a in (carr H1) /\ (carr H2)

then a in carr H2 by XBOOLE_0:def 4;

then a in H2 by STRUCT_0:def 5;

then (G ^ o) . a in H2 by Lm9;

then A10: (G ^ o) . a in carr H2 by STRUCT_0:def 5;

a in carr H1 by A9, XBOOLE_0:def 4;

then a in H1 by STRUCT_0:def 5;

then (G ^ o) . a in H1 by Lm9;

then (G ^ o) . a in carr H1 by STRUCT_0:def 5;

hence (G ^ o) . a in (carr H1) /\ (carr H2) by A10, XBOOLE_0:def 4; :: thesis: verum

A11: now :: thesis: for g being Element of G st g in (carr H1) /\ (carr H2) holds

g " in (carr H1) /\ (carr H2)

1_ G in H1
by Lm17;g " in (carr H1) /\ (carr H2)

let g be Element of G; :: thesis: ( g in (carr H1) /\ (carr H2) implies g " in (carr H1) /\ (carr H2) )

assume A12: g in (carr H1) /\ (carr H2) ; :: thesis: g " in (carr H1) /\ (carr H2)

then g in carr H2 by XBOOLE_0:def 4;

then g in H2 by STRUCT_0:def 5;

then g " in H2 by Lm19;

then A13: g " in carr H2 by STRUCT_0:def 5;

g in carr H1 by A12, XBOOLE_0:def 4;

then g in H1 by STRUCT_0:def 5;

then g " in H1 by Lm19;

then g " in carr H1 by STRUCT_0:def 5;

hence g " in (carr H1) /\ (carr H2) by A13, XBOOLE_0:def 4; :: thesis: verum

end;assume A12: g in (carr H1) /\ (carr H2) ; :: thesis: g " in (carr H1) /\ (carr H2)

then g in carr H2 by XBOOLE_0:def 4;

then g in H2 by STRUCT_0:def 5;

then g " in H2 by Lm19;

then A13: g " in carr H2 by STRUCT_0:def 5;

g in carr H1 by A12, XBOOLE_0:def 4;

then g in H1 by STRUCT_0:def 5;

then g " in H1 by Lm19;

then g " in carr H1 by STRUCT_0:def 5;

hence g " in (carr H1) /\ (carr H2) by A13, XBOOLE_0:def 4; :: thesis: verum

then 1_ G in the carrier of H1 by STRUCT_0:def 5;

then (carr H1) /\ (carr H2) <> {} by A1, XBOOLE_0:def 4;

hence ex b