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

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