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