let G be Group; :: thesis: for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1
let H1, H2 be Subgroup of G; :: thesis: H1 /\ H2 is Subgroup of H1
( the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 & the carrier of H1 /\ the carrier of H2 c= the carrier of H1 ) by Th97, XBOOLE_1:17;
hence H1 /\ H2 is Subgroup of H1 by Th66; :: thesis: verum