let G be Group; :: thesis: for H1, H2 being Subgroup of G holds the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2
let H1, H2 be Subgroup of G; :: thesis: the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2
the carrier of H2 = carr H2 by GROUP_2:def 9;
then the carrier of H1 /\ the carrier of H2 = (carr H1) /\ (carr H2) by GROUP_2:def 9;
hence the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 by GROUP_2:def 10; :: thesis: verum