let G be Group; :: thesis: for N, H being Subgroup of G holds N ` H c= N ~ H
let N, H be Subgroup of G; :: thesis: N ` H c= N ~ H
A1: N ` H c= carr H by Th53;
carr H c= N ~ H by Th54;
hence N ` H c= N ~ H by A1; :: thesis: verum