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