let G be Group; :: thesis: for A being non empty Subset of
for N being Subgroup of G holds N ~ (N ` A) c= A
let A be non empty Subset of ; :: thesis: for N being Subgroup of G holds N ~ (N ` A) c= A
let N be Subgroup of G; :: thesis: N ~ (N ` A) c= A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ (N ` A) or x in A )
assume A1: x in N ~ (N ` A) ; :: thesis: x in A
then reconsider x' = x as Element of ;
x' * N meets N ` A by A1, Th33;
then consider y being set such that
A2: ( y in x' * N & y in N ` A ) by XBOOLE_0:3;
reconsider y' = y as Element of by A2;
y' * N c= A by A2, Th12;
then A3: x' * N c= A by A2, Th2;
x' in x' * N by GROUP_2:130;
hence x in A by A3; :: thesis: verum