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

for N being Subgroup of G holds N ~ (N ` A) c= A

let A be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ~ (N ` A) c= A

let N be Subgroup of G; :: thesis: N ~ (N ` A) c= A

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

assume A1: x in N ~ (N ` A) ; :: thesis: x in A

then reconsider x9 = x as Element of G ;

x9 * N meets N ` A by A1, Th33;

then consider y being object such that

A2: ( y in x9 * N & y in N ` A ) by XBOOLE_0:3;

reconsider y9 = y as Element of G by A2;

y9 * N c= A by A2, Th12;

then A3: x9 * N c= A by A2, Th2;

x9 in x9 * N by GROUP_2:108;

hence x in A by A3; :: thesis: verum

for N being Subgroup of G holds N ~ (N ` A) c= A

let A be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ~ (N ` A) c= A

let N be Subgroup of G; :: thesis: N ~ (N ` A) c= A

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

assume A1: x in N ~ (N ` A) ; :: thesis: x in A

then reconsider x9 = x as Element of G ;

x9 * N meets N ` A by A1, Th33;

then consider y being object such that

A2: ( y in x9 * N & y in N ` A ) by XBOOLE_0:3;

reconsider y9 = y as Element of G by A2;

y9 * N c= A by A2, Th12;

then A3: x9 * N c= A by A2, Th2;

x9 in x9 * N by GROUP_2:108;

hence x in A by A3; :: thesis: verum