theorem :: GROUP_2:144

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