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

N1 ~ N1 c= N2 ~ N2

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

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

then A2: N2 ~ N1 c= N2 ~ N2 by Th56;

N1 ~ N1 c= N2 ~ N1 by A1, Th57;

hence N1 ~ N1 c= N2 ~ N2 by A2; :: thesis: verum

N1 ~ N1 c= N2 ~ N2

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

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

then A2: N2 ~ N1 c= N2 ~ N2 by Th56;

N1 ~ N1 c= N2 ~ N1 by A1, Th57;

hence N1 ~ N1 c= N2 ~ N2 by A2; :: thesis: verum