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

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

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

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

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

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

then reconsider x = x as Element of G ;

x * N c= N ~ (N ` A)

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

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

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

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

proof

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

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

then consider x1 being Element of G such that

A1: ( x1 = x & x1 * N c= N ~ (N ` A) ) ;

x1 in x1 * N by GROUP_2:108;

then x1 * N meets N ` A by A1, Th33;

then consider y being object such that

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

reconsider y = y as Element of G by A2;

y * N c= A by A2, Th12;

then x1 * N c= A by A2, Th2;

hence x in N ` A by A1; :: thesis: verum

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

then consider x1 being Element of G such that

A1: ( x1 = x & x1 * N c= N ~ (N ` A) ) ;

x1 in x1 * N by GROUP_2:108;

then x1 * N meets N ` A by A1, Th33;

then consider y being object such that

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

reconsider y = y as Element of G by A2;

y * N c= A by A2, Th12;

then x1 * N c= A by A2, Th2;

hence x in N ` A by A1; :: thesis: verum

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

then reconsider x = x as Element of G ;

x * N c= N ~ (N ` A)

proof

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

assume A4: y in x * N ; :: thesis: y in N ~ (N ` A)

then reconsider y = y as Element of G ;

y * N = x * N by A4, Th2;

then x in y * N by GROUP_2:108;

then y * N meets N ` A by A3, XBOOLE_0:3;

hence y in N ~ (N ` A) ; :: thesis: verum

end;assume A4: y in x * N ; :: thesis: y in N ~ (N ` A)

then reconsider y = y as Element of G ;

y * N = x * N by A4, Th2;

then x in y * N by GROUP_2:108;

then y * N meets N ` A by A3, XBOOLE_0:3;

hence y in N ~ (N ` A) ; :: thesis: verum