let G be Group; :: thesis: for A being non empty Subset of G
for N being Subgroup of G holds N ` (N ` A) = N ` A
let A be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ` (N ` A) = N ` A
let N be Subgroup of G; :: thesis: N ` (N ` A) = N ` A
thus N ` (N ` A) c= N ` A :: according to XBOOLE_0:def 10 :: thesis: 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 ` A )
assume x in N ` (N ` A) ; :: thesis: x in N ` A
then consider y being Element of G such that
A1: ( y = x & y * N c= N ` A ) ;
y in y * N by GROUP_2:108;
hence x in N ` A by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ` A or x in N ` (N ` A) )
assume A2: x in N ` A ; :: thesis: x in N ` (N ` A)
then reconsider x9 = x as Element of G ;
A3: x9 * N c= A by A2, Th12;
x9 * N c= N ` A

proof

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

end;

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