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