theorem :: GROUP_1A:187

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