let G be addGroup; :: thesis: Right_Cosets ((0). G) = { {a} where a is Element of G : verum }
set A = { {a} where a is Element of G : verum } ;
thus Right_Cosets ((0). G) c= { {a} where a is Element of G : verum } :: according to XBOOLE_0:def 10 :: thesis: { {a} where a is Element of G : verum } c= Right_Cosets ((0). G)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Right_Cosets ((0). G) or x in { {a} where a is Element of G : verum } )
assume A1: x in Right_Cosets ((0). G) ; :: thesis: x in { {a} where a is Element of G : verum }
then reconsider X = x as Subset of G ;
consider g being Element of G such that
A2: X = ((0). G) + g by A1, Def16;
x = {g} by A2, Th110;
hence x in { {a} where a is Element of G : verum } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { {a} where a is Element of G : verum } or x in Right_Cosets ((0). G) )
assume x in { {a} where a is Element of G : verum } ; :: thesis: x in Right_Cosets ((0). G)
then consider a being Element of G such that
A3: x = {a} ;
((0). G) + a = {a} by Th110;
hence x in Right_Cosets ((0). G) by A3, Def16; :: thesis: verum