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

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

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

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

thus N ~ A c= N ~ (N ~ A) :: according to XBOOLE_0:def 10 :: thesis: N ~ (N ~ A) c= N ~ A

assume A2: x in N ~ (N ~ A) ; :: thesis: x in N ~ A

then reconsider x9 = x as Element of G ;

x9 * N meets N ~ A by A2, Th32;

then consider y being object such that

A3: ( y in x9 * N & y in N ~ A ) by XBOOLE_0:3;

reconsider y9 = y as Element of G by A3;

A4: y9 * N meets A by A3, Th14;

y9 * N = x9 * N by A3, Th2;

hence x in N ~ A by A4; :: thesis: verum

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

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

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

thus N ~ A c= N ~ (N ~ A) :: according to XBOOLE_0:def 10 :: thesis: N ~ (N ~ A) c= N ~ A

proof

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

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

then reconsider x = x as Element of G ;

x in x * N by GROUP_2:108;

then x * N meets N ~ A by A1, XBOOLE_0:3;

hence x in N ~ (N ~ A) ; :: thesis: verum

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

then reconsider x = x as Element of G ;

x in x * N by GROUP_2:108;

then x * N meets N ~ A by A1, XBOOLE_0:3;

hence x in N ~ (N ~ A) ; :: thesis: verum

assume A2: x in N ~ (N ~ A) ; :: thesis: x in N ~ A

then reconsider x9 = x as Element of G ;

x9 * N meets N ~ A by A2, Th32;

then consider y being object such that

A3: ( y in x9 * N & y in N ~ A ) by XBOOLE_0:3;

reconsider y9 = y as Element of G by A3;

A4: y9 * N meets A by A3, Th14;

y9 * N = x9 * N by A3, Th2;

hence x in N ~ A by A4; :: thesis: verum