for G being Group
for x being object
for N being normal Subgroup of G holds
( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) ) by Th13, Th14;