let G be Group; :: thesis: for A being non empty Subset of G
for N being Subgroup of G holds N ` A c= N ~ A
let A be non empty Subset of G; :: thesis: for N being Subgroup of G holds N ` A c= N ~ A
let N be Subgroup of G; :: thesis: N ` A c= N ~ A
A1: N ` A c= A by Th16;
A c= N ~ A by Th17;
hence N ` A c= N ~ A by A1, XBOOLE_1:1; :: thesis: verum