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))

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

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

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

then reconsider x = x as Element of G ;

x * N meets N ` (N ~ A) by A1, Th30;

then consider y being object such that

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

reconsider y = y as Element of G by A2;

y * N c= N ~ A by A2, Th31;

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

x in x * N by GROUP_2:108;

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

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

then reconsider x = x as Element of G ;

x * N meets N ` (N ~ A) by A1, Th30;

then consider y being object such that

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

reconsider y = y as Element of G by A2;

y * N c= N ~ A by A2, Th31;

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

x in x * N by GROUP_2:108;

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

proof

A c= N ` (N ~ A)

end;proof

hence
N ~ A c= N ~ (N ` (N ~ A))
by Th39; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in N ` (N ~ A) )

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

then reconsider x = x as Element of G ;

x * N c= N ~ A

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

then reconsider x = x as Element of G ;

x * N c= N ~ A

proof

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

assume A5: y in x * N ; :: thesis: y in N ~ A

then reconsider y = y as Element of G ;

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

then x in y * N by GROUP_2:108;

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

hence y in N ~ A ; :: thesis: verum

end;assume A5: y in x * N ; :: thesis: y in N ~ A

then reconsider y = y as Element of G ;

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

then x in y * N by GROUP_2:108;

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

hence y in N ~ A ; :: thesis: verum