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