let G be addGroup; :: thesis: ( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} )
set a = the Element of G;
A1: Left_Cosets ((Omega). G) c= { the carrier of G}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Left_Cosets ((Omega). G) or x in { the carrier of G} )
assume A2: 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
A3: X = a + ((Omega). G) by A2, Def15;
a + ((Omega). G) = the carrier of G by Th111;
hence x in { the carrier of G} by A3, TARSKI:def 1; :: thesis: verum

end;

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

proof

let x be object ; :: 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 Th111;
hence x in { the carrier of G} by A6, TARSKI:def 1; :: thesis: verum

end;

((Omega). G) + the Element of G = the carrier of G by Th111;
then A7: the carrier of G in Right_Cosets ((Omega). G) by Def16;
the Element of G + ((Omega). G) = the carrier of G by Th111;
then the carrier of G in Left_Cosets ((Omega). G) by Def15;
hence ( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} ) by A7, ZFMISC_1:31, A1, A4; :: thesis: verum