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

proof

consider a being Element of G;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of H or x in {(1_ G)} )
assume x in the carrier of H ; :: thesis: x in {(1_ G)}
then reconsider h = x as Element of H ;
A3: h in H by STRUCT_0:def 5;
reconsider h = h as Element of G by Th51;
a * H in Left_Cosets H by Def15;
then consider b being Element of G such that
A4: a * H = {b} by A1;
a * h in a * H by A3, Th125;
then A5: a * h = b by A4, TARSKI:def 1;
1_ G in H by Th55;
then a * (1_ G) in a * H by Th125;
then a * (1_ G) = b by A4, TARSKI:def 1;
then h = 1_ G by A5, GROUP_1:14;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

1_ G in H by Th55;
then 1_ G in the carrier of H by STRUCT_0:def 5;
then {(1_ G)} c= the carrier of H by ZFMISC_1:37;
then {(1_ G)} = the carrier of H by A2, XBOOLE_0:def 10;
hence H = (1). G by Def7; :: thesis: verum