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