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