text: let G be Group; :: thesis: for H being Subgroup of G
  for N being normal Subgroup of G st N is Subgroup of H holds
  ex M being strict Subgroup of G st the carrier of M = N ` H
  
  let H be Subgroup of G; :: thesis: for N being normal Subgroup of G st N is Subgroup of H holds
  ex M being strict Subgroup of G st the carrier of M = N ` H
  
  let N be normal Subgroup of G; :: thesis: ( N is Subgroup of H implies ex M being strict Subgroup of G st the carrier of M = N ` H )
  assume A1: N is Subgroup of H ; :: thesis: ex M being strict Subgroup of G st the carrier of M = N ` H
  A2: 1_ G in N ` H
  proof
  1_ G in N by GROUP_2:46;
  then A3: (1_ G) * N = carr N by GROUP_2:113;
  carr N c= carr H by ;
  hence 1_ G in N ` H by A3; :: thesis: verum
  end;
  A4: for x, y being Element of G st x in N ` H & y in N ` H holds
  x * y in N ` H
  proof
  let x, y be Element of G; :: thesis: ( x in N ` H & y in N ` H implies x * y in N ` H )
  assume ( x in N ` H & y in N ` H ) ; :: thesis: x * y in N ` H
  then ( x * N c= carr H & y * N c= carr H ) by Th49;
  then A5: (x * N) * (y * N) c= (carr H) * (carr H) by GROUP_3:4;
  A6: (x * N) * (y * N) = (x * y) * N by Th1;
  (carr H) * (carr H) = carr H by GROUP_2:76;
  hence x * y in N ` H by A5, A6; :: thesis: verum
  end;
  for x being Element of G st x in N ` H holds
  x " in N ` H
  proof
  let x be Element of G; :: thesis: ( x in N ` H implies x " in N ` H )
  assume x in N ` H ; :: thesis: x " in N ` H
  then A7: x * N c= carr H by Th49;
  x in x * N by GROUP_2:108;
  then x in H by ;
  then x " in H by GROUP_2:51;
  then A8: (x ") * H = carr H by GROUP_2:113;
  (x ") * N c= (x ") * H by ;
  hence x " in N ` H by A8; :: thesis: verum
  end;
  hence ex M being strict Subgroup of G st the carrier of M = N ` H by ; :: thesis: verum