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