theorem :: GROUP_2:141

for G being Group
for H being strict Subgroup of G st Right_Cosets H = { {a} where a is Element of G : verum } holds
H = (1). G