let G be Group; :: thesis: for H1, H2 being strict Subgroup of G holds the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2)
let H1, H2 be strict Subgroup of G; :: thesis: the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2)
( (carr G) . H1 = the carrier of H1 & (carr G) . H2 = the carrier of H2 ) by Def1;
hence the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2) by Th1; :: thesis: verum