let G be strict addGroup; :: thesis: for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds
H = G
let H be strict Subgroup of G; :: thesis: ( Right_Cosets H = { the carrier of G} implies H = G )
assume Right_Cosets H = { the carrier of G} ; :: thesis: H = G
then A1: the carrier of G in Right_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 = H + a by A1, Def16;
now :: thesis: for g being Element of G holds g in H
let g be Element of G; :: thesis: g in H
ex b being Element of G st
( g + a = b + a & b in H ) by A2, Th104;
hence g in H by Th6; :: thesis: verum
end;
hence H = G by Th62; :: thesis: verum