let G be Group; :: thesis: for H, N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds

N1 ~ H c= N2 ~ H

let H, N1, N2 be Subgroup of G; :: thesis: ( N1 is Subgroup of N2 implies N1 ~ H c= N2 ~ H )

assume A1: N1 is Subgroup of N2 ; :: thesis: N1 ~ H c= N2 ~ H

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 ~ H or x in N2 ~ H )

assume A2: x in N1 ~ H ; :: thesis: x in N2 ~ H

then reconsider x = x as Element of G ;

x * N1 meets carr H by A2, Th51;

then x * N2 meets carr H by A1, GROUP_3:6, XBOOLE_1:63;

hence x in N2 ~ H ; :: thesis: verum

N1 ~ H c= N2 ~ H

let H, N1, N2 be Subgroup of G; :: thesis: ( N1 is Subgroup of N2 implies N1 ~ H c= N2 ~ H )

assume A1: N1 is Subgroup of N2 ; :: thesis: N1 ~ H c= N2 ~ H

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 ~ H or x in N2 ~ H )

assume A2: x in N1 ~ H ; :: thesis: x in N2 ~ H

then reconsider x = x as Element of G ;

x * N1 meets carr H by A2, Th51;

then x * N2 meets carr H by A1, GROUP_3:6, XBOOLE_1:63;

hence x in N2 ~ H ; :: thesis: verum