set A = (carr H1) /\ (carr H2);
A1: 0_ G in H2 by Th46;
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)
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; :: thesis: verum
end;
A5: now :: thesis: for g being Element of G st g in (carr H1) /\ (carr H2) holds
- 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; :: thesis: verum
end;
0_ G in H1 by Th46;
then (carr H1) /\ (carr H2) <> {} by A1, XBOOLE_0:def 4;
hence ex b1 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) by A2, A5, Th52; :: thesis: verum