for G being Group holds
( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} )