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 object ; :: 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

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 object ; :: 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