let G be Group; :: thesis: ( Left_Cosets ((Omega). G) = {the carrier of G} & Right_Cosets ((Omega). G) = {the carrier of G} )
consider a being Element of G;
( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G ) by Th134;
then ( the carrier of G in Left_Cosets ((Omega). G) & the carrier of G in Right_Cosets ((Omega). G) ) by Def15, Def16;
then A1: ( {the carrier of G} c= Left_Cosets ((Omega). G) & {the carrier of G} c= Right_Cosets ((Omega). G) ) by ZFMISC_1:37;
A2: Left_Cosets ((Omega). G) c= {the carrier of G}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Left_Cosets ((Omega). G) or x in {the carrier of G} )
assume A3: x in Left_Cosets ((Omega). G) ; :: thesis: x in {the carrier of G}
then reconsider X = x as Subset of G ;
consider a being Element of G such that
A4: X = a * ((Omega). G) by A3, Def15;
a * ((Omega). G) = the carrier of G by Th134;
hence x in {the carrier of G} by A4, TARSKI:def 1; :: thesis: verum

end;

Right_Cosets ((Omega). G) c= {the carrier of G}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Right_Cosets ((Omega). G) or x in {the carrier of G} )
assume A5: x in Right_Cosets ((Omega). G) ; :: thesis: x in {the carrier of G}
then reconsider X = x as Subset of G ;
consider a being Element of G such that
A6: X = ((Omega). G) * a by A5, Def16;
((Omega). G) * a = the carrier of G by Th134;
hence x in {the carrier of G} by A6, TARSKI:def 1; :: thesis: verum

end;

hence ( Left_Cosets ((Omega). G) = {the carrier of G} & Right_Cosets ((Omega). G) = {the carrier of G} ) by A1, A2, XBOOLE_0:def 10; :: thesis: verum