let G be Group; :: 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}

then the carrier of G in Right_Cosets ((Omega). G) by Def16;

then A7: { the carrier of G} c= Right_Cosets ((Omega). G) by ZFMISC_1:31;

the Element of G * ((Omega). G) = the carrier of G by Th111;

then the carrier of G in Left_Cosets ((Omega). G) by Def15;

then { the carrier of G} c= Left_Cosets ((Omega). G) by ZFMISC_1:31;

hence ( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} ) by A7, A1, A4; :: thesis: verum

set a = the Element of G;

A1: Left_Cosets ((Omega). G) c= { the carrier of G}

proof

A4:
Right_Cosets ((Omega). G) c= { the carrier of G}
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;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

proof

((Omega). G) * the Element of G = the carrier of G
by Th111;
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;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

then the carrier of G in Right_Cosets ((Omega). G) by Def16;

then A7: { the carrier of G} c= Right_Cosets ((Omega). G) by ZFMISC_1:31;

the Element of G * ((Omega). G) = the carrier of G by Th111;

then the carrier of G in Left_Cosets ((Omega). G) by Def15;

then { the carrier of G} c= Left_Cosets ((Omega). G) by ZFMISC_1:31;

hence ( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} ) by A7, A1, A4; :: thesis: verum