let G be Group; :: thesis: ( Left_Cosets () = { the carrier of G} & Right_Cosets () = { the carrier of G} )
set a = the Element of G;
A1: Left_Cosets () c= { the carrier of G}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Left_Cosets () or x in { the carrier of G} )
assume A2: x in Left_Cosets () ; :: 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 * () by ;
a * () = the carrier of G by Th111;
hence x in { the carrier of G} by ; :: thesis: verum
end;
A4: Right_Cosets () c= { the carrier of G}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Right_Cosets () or x in { the carrier of G} )
assume A5: x in Right_Cosets () ; :: 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 = () * a by ;
((Omega). G) * a = the carrier of G by Th111;
hence x in { the carrier of G} by ; :: thesis: verum
end;
((Omega). G) * the Element of G = the carrier of G by Th111;
then the carrier of G in Right_Cosets () by Def16;
then A7: { the carrier of G} c= Right_Cosets () by ZFMISC_1:31;
the Element of G * () = the carrier of G by Th111;
then the carrier of G in Left_Cosets () by Def15;
then { the carrier of G} c= Left_Cosets () by ZFMISC_1:31;
hence ( Left_Cosets () = { the carrier of G} & Right_Cosets () = { the carrier of G} ) by A7, A1, A4; :: thesis: verum