let G be Group; :: thesis: Left_Cosets ((1). G) = { {a} where a is Element of G : verum }

set A = { {a} where a is Element of G : verum } ;

thus Left_Cosets ((1). 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= Left_Cosets ((1). G)

assume x in { {a} where a is Element of G : verum } ; :: thesis: x in Left_Cosets ((1). G)

then consider a being Element of G such that

A3: x = {a} ;

a * ((1). G) = {a} by Th110;

hence x in Left_Cosets ((1). G) by A3, Def15; :: thesis: verum

set A = { {a} where a is Element of G : verum } ;

thus Left_Cosets ((1). 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= Left_Cosets ((1). G)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { {a} where a is Element of G : verum } or x in Left_Cosets ((1). G) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Left_Cosets ((1). G) or x in { {a} where a is Element of G : verum } )

assume A1: x in Left_Cosets ((1). 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 = g * ((1). G) by A1, Def15;

x = {g} by A2, Th110;

hence x in { {a} where a is Element of G : verum } ; :: thesis: verum

end;assume A1: x in Left_Cosets ((1). 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 = g * ((1). G) by A1, Def15;

x = {g} by A2, Th110;

hence x in { {a} where a is Element of G : verum } ; :: thesis: verum

assume x in { {a} where a is Element of G : verum } ; :: thesis: x in Left_Cosets ((1). G)

then consider a being Element of G such that

A3: x = {a} ;

a * ((1). G) = {a} by Th110;

hence x in Left_Cosets ((1). G) by A3, Def15; :: thesis: verum