theorem :: GROUP_11:65

for G being Group
for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds
(N1 ` H) /\ (N2 ` H) c= N ` H