let G be Group; :: thesis: for A being non empty Subset of G
for N being Subgroup of G holds A c= N ~ A
let A be non empty Subset of G; :: thesis: for N being Subgroup of G holds A c= N ~ A
let N be Subgroup of G; :: thesis: A c= N ~ A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in N ~ A )
assume A1: x in A ; :: thesis: x in N ~ A
then reconsider x9 = x as Element of G ;
x9 in x9 * N by GROUP_2:108;
then x9 * N meets A by A1, XBOOLE_0:3;
hence x in N ~ A ; :: thesis: verum