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

end;

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