let G be Group; :: thesis: for A being non empty Subset of G
for N being Subgroup of G holds N ` (N ` A) = N ~ (N ` A)
let A be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ` (N ` A) = N ~ (N ` A)
let N be Subgroup of G; :: thesis: N ` (N ` A) = N ~ (N ` A)
thus N ` (N ` A) c= N ~ (N ` A) :: according to XBOOLE_0:def 10 :: thesis: N ~ (N ` A) c= N ` (N ` A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ` (N ` A) or x in N ~ (N ` A) )
assume A1: x in N ` (N ` A) ; :: thesis: x in N ~ (N ` A)
then reconsider x = x as Element of G ;
A2: x * N c= N ` A by A1, Th41;
x in x * N by GROUP_2:108;
then x * N meets N ` A by A2, XBOOLE_0:3;
hence x in N ~ (N ` A) ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ (N ` A) or x in N ` (N ` A) )
assume A3: x in N ~ (N ` A) ; :: thesis: x in N ` (N ` A)
then reconsider x = x as Element of G ;
x * N meets N ` A by A3, Th33;
then consider z being object such that
A4: ( z in x * N & z in N ` A ) by XBOOLE_0:3;
reconsider z = z as Element of G by A4;
z * N c= A by A4, Th12;
then A5: x * N c= A by A4, Th2;
x * N c= N ` A

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x * N or y in N ` A )
assume A6: y in x * N ; :: thesis: y in N ` A
then reconsider y = y as Element of G ;
x * N = y * N by A6, Th2;
hence y in N ` A by A5; :: thesis: verum

end;

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