reconsider H = H1 /\ H2 as Subgroup of H1 by GROUP_2:88;
H is p -commutative-group-like ;
hence H1 /\ H2 is p -commutative-group-like ; :: thesis: verum