for G being Group
for x being object
for N being normal Subgroup of G st x in Cosets N holds
ex a being Element of G st
( x = a * N & x = N * a )