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

proof

let x be set ; :: 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 " & h in {g} ) ;
h = g by A1, TARSKI:def 1;
hence x in {(g " )} by A1, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(g " )} or x in {g} " )
assume x in {(g " )} ; :: thesis: x in {g} "
then ( x = g " & g in {g} ) by TARSKI:def 1;
hence x in {g} " ; :: thesis: verum