let G be Group; :: thesis: for g being Element of G holds {g} " = {(g ")}

let g be Element of G; :: thesis: {g} " = {(g ")}

thus {g} " c= {(g ")} :: according to XBOOLE_0:def 10 :: thesis: {(g ")} c= {g} "

assume x in {(g ")} ; :: thesis: x in {g} "

then A3: x = g " by TARSKI:def 1;

g in {g} by TARSKI:def 1;

hence x in {g} " by A3; :: thesis: verum

let g be Element of G; :: thesis: {g} " = {(g ")}

thus {g} " c= {(g ")} :: according to XBOOLE_0:def 10 :: thesis: {(g ")} c= {g} "

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(g ")} or x in {g} " )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {g} " or x in {(g ")} )

assume x in {g} " ; :: thesis: x in {(g ")}

then consider h being Element of G such that

A1: x = h " and

A2: h in {g} ;

h = g by A2, TARSKI:def 1;

hence x in {(g ")} by A1, TARSKI:def 1; :: thesis: verum

end;assume x in {g} " ; :: thesis: x in {(g ")}

then consider h being Element of G such that

A1: x = h " and

A2: h in {g} ;

h = g by A2, TARSKI:def 1;

hence x in {(g ")} by A1, TARSKI:def 1; :: thesis: verum

assume x in {(g ")} ; :: thesis: x in {g} "

then A3: x = g " by TARSKI:def 1;

g in {g} by TARSKI:def 1;

hence x in {g} " by A3; :: thesis: verum