let G be Group; :: thesis: for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds
(N1 ` H) /\ (N2 ` H) c= N ` H
let H be Subgroup of G; :: thesis: for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds
(N1 ` H) /\ (N2 ` H) c= N ` H
let N, N1, N2 be Subgroup of G; :: thesis: ( N = N1 /\ N2 implies (N1 ` H) /\ (N2 ` H) c= N ` H )
assume N = N1 /\ N2 ; :: thesis: (N1 ` H) /\ (N2 ` H) c= N ` H
then A1: ( N is Subgroup of N1 & N is Subgroup of N2 ) by GROUP_2:88;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N1 ` H) /\ (N2 ` H) or x in N ` H )
assume x in (N1 ` H) /\ (N2 ` H) ; :: thesis: x in N ` H
then A2: ( x in N1 ` H & x in N2 ` H ) by XBOOLE_0:def 4;
( N1 ` H c= N ` H & N2 ` H c= N ` H ) by A1, Th60;
hence x in N ` H by A2; :: thesis: verum