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 meets carr H1 by A2, Th51;
then x * N meets carr H2 by A1, XBOOLE_1:63;
hence x in N ~ H2 ; :: thesis: verum