let G be strict Group; :: thesis: for H being strict Subgroup of G st Left_Cosets H = { the carrier of G} holds

H = G

let H be strict Subgroup of G; :: thesis: ( Left_Cosets H = { the carrier of G} implies H = G )

assume Left_Cosets H = { the carrier of G} ; :: thesis: H = G

then A1: the carrier of G in Left_Cosets H by TARSKI:def 1;

then reconsider T = the carrier of G as Subset of G ;

consider a being Element of G such that

A2: T = a * H by A1, Def15;

H = G

let H be strict Subgroup of G; :: thesis: ( Left_Cosets H = { the carrier of G} implies H = G )

assume Left_Cosets H = { the carrier of G} ; :: thesis: H = G

then A1: the carrier of G in Left_Cosets H by TARSKI:def 1;

then reconsider T = the carrier of G as Subset of G ;

consider a being Element of G such that

A2: T = a * H by A1, Def15;

now :: thesis: for g being Element of G holds g in H

hence
H = G
by Th62; :: thesis: verumlet g be Element of G; :: thesis: g in H

ex b being Element of G st

( a * g = a * b & b in H ) by A2, Th103;

hence g in H by GROUP_1:6; :: thesis: verum

end;ex b being Element of G st

( a * g = a * b & b in H ) by A2, Th103;

hence g in H by GROUP_1:6; :: thesis: verum