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