theorem Th142: :: GROUP_1A:188

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