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

1_ G in H2 by Th46;

then A1: 1_ G in the carrier of H2 ;

then 1_ G in the carrier of H1 ;

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

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

1_ G in H2 by Th46;

then A1: 1_ G in the carrier of H2 ;

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 A3: ( g1 in (carr H1) /\ (carr H2) & g2 in (carr H1) /\ (carr H2) ) ; :: thesis: g1 * g2 in (carr H1) /\ (carr H2)

then ( g1 in carr H2 & g2 in carr H2 ) by XBOOLE_0:def 4;

then A4: g1 * g2 in carr H2 by Th74;

( g1 in carr H1 & g2 in carr H1 ) by A3, XBOOLE_0:def 4;

then g1 * g2 in carr H1 by Th74;

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

end;assume A3: ( g1 in (carr H1) /\ (carr H2) & g2 in (carr H1) /\ (carr H2) ) ; :: thesis: g1 * g2 in (carr H1) /\ (carr H2)

then ( g1 in carr H2 & g2 in carr H2 ) by XBOOLE_0:def 4;

then A4: g1 * g2 in carr H2 by Th74;

( g1 in carr H1 & g2 in carr H1 ) by A3, XBOOLE_0:def 4;

then g1 * g2 in carr H1 by Th74;

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

A5: 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 Th46;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 A6: g in (carr H1) /\ (carr H2) ; :: thesis: g " in (carr H1) /\ (carr H2)

then g in carr H2 by XBOOLE_0:def 4;

then A7: g " in carr H2 by Th75;

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

then g " in carr H1 by Th75;

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

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

then g in carr H2 by XBOOLE_0:def 4;

then A7: g " in carr H2 by Th75;

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

then g " in carr H1 by Th75;

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

then 1_ G in the carrier of H1 ;

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

hence ex b