theorem :: GROUP_1A:190

for G being strict addGroup
for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds
H = G