theorem Th18: :: LATSUBGR:18
for G being Group
for H1, H2 being strict Subgroup of G holds the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2)