theorem Th138: :: GROUP_2:138

for G being Group holds Left_Cosets ((1). G) = { {a} where a is Element of G : verum }