reconsider H1 = G1 /\ G2 as Subgroup of G1 by GROUP_2:88;
H1 is p -group ;
hence G1 /\ G2 is p -group ; :: thesis: verum