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

for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B)

let A, B be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B)

let N be Subgroup of G; :: thesis: N ` (A /\ B) = (N ` A) /\ (N ` B)

thus N ` (A /\ B) c= (N ` A) /\ (N ` B) :: according to XBOOLE_0:def 10 :: thesis: (N ` A) /\ (N ` B) c= N ` (A /\ B)

assume A3: x in (N ` A) /\ (N ` B) ; :: thesis: x in N ` (A /\ B)

then reconsider x = x as Element of G ;

( x in N ` A & x in N ` B ) by A3, XBOOLE_0:def 4;

then ( x * N c= A & x * N c= B ) by Th12;

then x * N c= A /\ B by XBOOLE_1:19;

hence x in N ` (A /\ B) ; :: thesis: verum

for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B)

let A, B be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B)

let N be Subgroup of G; :: thesis: N ` (A /\ B) = (N ` A) /\ (N ` B)

thus N ` (A /\ B) c= (N ` A) /\ (N ` B) :: according to XBOOLE_0:def 10 :: thesis: (N ` A) /\ (N ` B) c= N ` (A /\ B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N ` A) /\ (N ` B) or x in N ` (A /\ B) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ` (A /\ B) or x in (N ` A) /\ (N ` B) )

assume A1: x in N ` (A /\ B) ; :: thesis: x in (N ` A) /\ (N ` B)

then reconsider x = x as Element of G ;

consider x1 being Element of G such that

A2: ( x1 = x & x1 * N c= A /\ B ) by A1;

( x * N c= A & x * N c= B ) by A2, XBOOLE_1:18;

then ( x in N ` A & x in N ` B ) ;

hence x in (N ` A) /\ (N ` B) by XBOOLE_0:def 4; :: thesis: verum

end;assume A1: x in N ` (A /\ B) ; :: thesis: x in (N ` A) /\ (N ` B)

then reconsider x = x as Element of G ;

consider x1 being Element of G such that

A2: ( x1 = x & x1 * N c= A /\ B ) by A1;

( x * N c= A & x * N c= B ) by A2, XBOOLE_1:18;

then ( x in N ` A & x in N ` B ) ;

hence x in (N ` A) /\ (N ` B) by XBOOLE_0:def 4; :: thesis: verum

assume A3: x in (N ` A) /\ (N ` B) ; :: thesis: x in N ` (A /\ B)

then reconsider x = x as Element of G ;

( x in N ` A & x in N ` B ) by A3, XBOOLE_0:def 4;

then ( x * N c= A & x * N c= B ) by Th12;

then x * N c= A /\ B by XBOOLE_1:19;

hence x in N ` (A /\ B) ; :: thesis: verum