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

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

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

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

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

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

assume A1: A c= N ` (N ~ A) ; :: thesis: N ~ A c= N ~ (N ` (N ~ A))

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

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

then reconsider x = x as Element of G ;

x * N meets A by A2, Th14;

then x * N meets N ` (N ~ A) by A1, XBOOLE_1:63;

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

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

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

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

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

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

assume A1: A c= N ` (N ~ A) ; :: thesis: N ~ A c= N ~ (N ` (N ~ A))

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

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

then reconsider x = x as Element of G ;

x * N meets A by A2, Th14;

then x * N meets N ` (N ~ A) by A1, XBOOLE_1:63;

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