let G be addGroup; :: thesis: for H being strict Subgroup of G st Right_Cosets H = { {a} where a is Element of G : verum } holds
H = (0). G
let H be strict Subgroup of G; :: thesis: ( Right_Cosets H = { {a} where a is Element of G : verum } implies H = (0). G )
assume A1: Right_Cosets H = { {a} where a is Element of G : verum } ; :: thesis: H = (0). G
A2: the carrier of H c= {(0_ G)}

proof

set a = the Element of G;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of H or x in {(0_ G)} )
assume x in the carrier of H ; :: thesis: x in {(0_ G)}
then reconsider h = x as Element of H ;
A3: h in H ;
reconsider h = h as Element of G by Th41, STRUCT_0:def 5;
H + the Element of G in Right_Cosets H by Def16;
then consider b being Element of G such that
A4: H + the Element of G = {b} by A1;
h + the Element of G in H + the Element of G by A3, Th104;
then A5: h + the Element of G = b by A4, TARSKI:def 1;
(0_ G) + the Element of G in H + the Element of G by Th46, Th104;
then (0_ G) + the Element of G = b by A4, TARSKI:def 1;
then h = 0_ G by A5, Th6;
hence x in {(0_ G)} by TARSKI:def 1; :: thesis: verum

end;

0_ G in H by Th46;
then {(0_ G)} = the carrier of H by A2, ZFMISC_1:31;
hence H = (0). G by Def7; :: thesis: verum