let G be Group; :: thesis: for A being non empty Subset of G

for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

(N1 ` A) /\ (N2 ` A) c= N ` A

let A be non empty Subset of G; :: thesis: for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

(N1 ` A) /\ (N2 ` A) c= N ` A

let N, N1, N2 be Subgroup of G; :: thesis: ( N = N1 /\ N2 implies (N1 ` A) /\ (N2 ` A) c= N ` A )

assume N = N1 /\ N2 ; :: thesis: (N1 ` A) /\ (N2 ` A) c= N ` A

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 ` A) /\ (N2 ` A) or x in N ` A )

assume x in (N1 ` A) /\ (N2 ` A) ; :: thesis: x in N ` A

then A2: ( x in N1 ` A & x in N2 ` A ) by XBOOLE_0:def 4;

( N1 ` A c= N ` A & N2 ` A c= N ` A ) by A1, Th25;

hence x in N ` A by A2; :: thesis: verum

for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

(N1 ` A) /\ (N2 ` A) c= N ` A

let A be non empty Subset of G; :: thesis: for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

(N1 ` A) /\ (N2 ` A) c= N ` A

let N, N1, N2 be Subgroup of G; :: thesis: ( N = N1 /\ N2 implies (N1 ` A) /\ (N2 ` A) c= N ` A )

assume N = N1 /\ N2 ; :: thesis: (N1 ` A) /\ (N2 ` A) c= N ` A

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 ` A) /\ (N2 ` A) or x in N ` A )

assume x in (N1 ` A) /\ (N2 ` A) ; :: thesis: x in N ` A

then A2: ( x in N1 ` A & x in N2 ` A ) by XBOOLE_0:def 4;

( N1 ` A c= N ` A & N2 ` A c= N ` A ) by A1, Th25;

hence x in N ` A by A2; :: thesis: verum