let G be Group; :: thesis: for g, h being Element of G holds {g,h} " = {(g "),(h ")}
let g, h be Element of G; :: thesis: {g,h} " = {(g "),(h ")}
thus {g,h} " c= {(g "),(h ")} :: according to XBOOLE_0:def 10 :: thesis: {(g "),(h ")} c= {g,h} "

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {g,h} " or x in {(g "),(h ")} )
assume x in {g,h} " ; :: thesis: x in {(g "),(h ")}
then consider a being Element of G such that
A1: x = a " and
A2: a in {g,h} ;
( a = g or a = h ) by A2, TARSKI:def 2;
hence x in {(g "),(h ")} by A1, TARSKI:def 2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(g "),(h ")} or x in {g,h} " )
assume x in {(g "),(h ")} ; :: thesis: x in {g,h} "
then A3: ( x = g " or x = h " ) by TARSKI:def 2;
( g in {g,h} & h in {g,h} ) by TARSKI:def 2;
hence x in {g,h} " by A3; :: thesis: verum