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}
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 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