theorem Th143: :: GROUP_1A:189
for G being strict addGroup
for H being strict Subgroup of G st Left_Cosets H = { the carrier of G} holds
H = G