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 object ; :: 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 c= A by A2, Th12;

then x * N c= B by A1;

hence x in N ` B ; :: thesis: verum

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 object ; :: 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 c= A by A2, Th12;

then x * N c= B by A1;

hence x in N ` B ; :: thesis: verum