let G be Group; :: thesis: for N, H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds
N ` H1 c= N ` H2
let N, H1, H2 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 implies N ` H1 c= N ` H2 )
assume H1 is Subgroup of H2 ; :: thesis: N ` H1 c= N ` H2
then A1: carr H1 c= carr H2 by GROUP_2:def 5;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ` H1 or x in N ` H2 )
assume A2: x in N ` H1 ; :: thesis: x in N ` H2
then reconsider x = x as Element of G ;
x * N c= carr H1 by A2, Th49;
then x * N c= carr H2 by A1;
hence x in N ` H2 ; :: thesis: verum