let G be Group; :: thesis: for N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds
N2 ` N1 c= N1 ` N2
let N1, N2 be Subgroup of G; :: thesis: ( N1 is Subgroup of N2 implies N2 ` N1 c= N1 ` N2 )
assume A1: N1 is Subgroup of N2 ; :: thesis: N2 ` N1 c= N1 ` N2
then A2: N2 ` N1 c= N2 ` N2 by Th59;
N2 ` N2 c= N1 ` N2 by A1, Th60;
hence N2 ` N1 c= N1 ` N2 by A2; :: thesis: verum